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 Th9;
On Y c= sup Y by Def3;
then On X c= sup Y by A1;
hence sup X c= sup Y by Def3; :: thesis: verum