let X, Y be ext-real-membered set ; :: thesis: ( X c= Y & Y is bounded implies X is bounded )
assume A1: X c= Y ; :: thesis: ( not Y is bounded or X is bounded )
assume ( Y is bounded_below & Y is bounded_above ) ; :: according to XXREAL_2:def 11 :: thesis: X is bounded
hence ( X is bounded_below & X is bounded_above ) by A1, Th43, Th44; :: according to XXREAL_2:def 11 :: thesis: verum