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