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;

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;