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

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