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 ( On X c= On Y & On Y c= sup Y ) by Def7, Th11;
then ( On X c= sup Y & ( for A being Ordinal st On X c= A holds
sup X c= A ) ) by Def7, XBOOLE_1:1;
hence sup X c= sup Y ; :: thesis: verum