let X, Y be ext-real-membered set ; :: thesis: ( X c= Y & Y is bounded_below implies X is bounded_below )
assume A1: X c= Y ; :: thesis: ( not Y is bounded_below or X is bounded_below )
given r being Real such that A2: r is LowerBound of Y ; :: according to XXREAL_2:def 9 :: thesis: X is bounded_below
take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of X
thus r is LowerBound of X by A1, A2, Th5; :: thesis: verum