let X, Y be set ; :: thesis: ( X c= Y implies sup X c= sup Y )
assume X c= Y ; :: thesis: sup X c= sup Y
then A1: On X c= On Y by Th11;
On Y c= sup Y by Def7;
then On X c= sup Y by A1, XBOOLE_1:1;
hence sup X c= sup Y by Def7; :: thesis: verum