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 that
A1: X c= Y and
A2: Y is bounded_above ; :: thesis: upper_bound X <= upper_bound Y
for t being real number st t in X holds
t <= upper_bound Y by A1, A2, Def4;
hence upper_bound X <= upper_bound Y by Th62; :: thesis: verum