let X be non empty real-membered set ; :: thesis: for Y being real-membered set st X c= Y & Y is bounded_above holds
upper_bound X <= upper_bound Y
let Y be real-membered set ; :: thesis: ( X c= Y & Y is bounded_above implies upper_bound X <= upper_bound Y )
assume ( X c= Y & Y is bounded_above ) ; :: thesis: upper_bound X <= upper_bound Y
then for t being Real st t in X holds
t <= upper_bound Y by Def1;
hence upper_bound X <= upper_bound Y by Th45; :: thesis: verum