let X be non empty real-membered set ; :: thesis: for Y being real-membered set st X c= Y & Y is bounded_below holds
lower_bound Y <= lower_bound X
let Y be real-membered set ; :: thesis: ( X c= Y & Y is bounded_below implies lower_bound Y <= lower_bound X )
assume that
A1: X c= Y and
A2: Y is bounded_below ; :: thesis: lower_bound Y <= lower_bound X
for t being real number st t in X holds
t >= lower_bound Y by A1, A2, Def5;
hence lower_bound Y <= lower_bound X by Th60; :: thesis: verum