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 ( X c= Y & Y is bounded_below ) ; :: thesis: lower_bound Y <= lower_bound X
then for t being Real st t in X holds
t >= lower_bound Y by Def2;
hence lower_bound Y <= lower_bound X by Th43; :: thesis: verum