let X, Y be ext-real-membered set ; :: thesis: ( X c= Y implies sup X <= sup Y )
assume A1: X c= Y ; :: thesis: sup X <= sup Y
sup Y is UpperBound of Y by Def3;
then sup Y is UpperBound of X by A1, Th6;
hence sup X <= sup Y by Def3; :: thesis: verum