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