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

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