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

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