Properties - Predicates
reflexivity
definition
let X, Y be set;
redefine pred X c= Y;
reflexivity
proof
thus for x being set holds x c= x;
end;
end;
irreflexivity
definition
let X, Y be set;
redefine pred X c= Y;
irreflexivity
proof
thus for x being set holds not x c= x;
end;
end;
symmetry
definition
let X, Y be set;
redefine pred X c= Y;
symmetry
proof
thus for x, y being set st x c= y holds y c= x;
end;
end;
asymmetry
definition
let X, Y be set;
redefine pred X c= Y;
asymmetry
proof
thus for x, y being set st x c= y holds not y c= x;
end;
end;
connectedness
definition
let X, Y be set;
redefine pred X c= Y;
connectedness
proof
thus for x, y being set holds x c= y or y c= x;
end;
end;
Properties - Functors
commutativity
definition
let X, Y be set;
redefine func X + Y;
commutativity
proof
thus for x, y being set holds x + y = y + x;
end;
end;