let X, Y be Subset of REAL; :: thesis: ( X is bounded_below & Y is bounded_below implies X ++ Y is bounded_below )
assume X is bounded_below ; :: thesis: ( not Y is bounded_below or X ++ Y is bounded_below )
then consider r1 being real number such that
A1: r1 is LowerBound of X by XXREAL_2:def 9;
A2: for r being real number st r in X holds
r1 <= r by A1, XXREAL_2:def 2;
assume Y is bounded_below ; :: thesis: X ++ Y is bounded_below
then consider r2 being real number such that
A3: r2 is LowerBound of Y by XXREAL_2:def 9;
A4: for r being real number st r in Y holds
r2 <= r by A3, XXREAL_2:def 2;
take r1 + r2 ; :: according to XXREAL_2:def 9 :: thesis: r1 + r2 is LowerBound of X ++ Y
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in X ++ Y or r1 + r2 <= r )
assume r in X ++ Y ; :: thesis: r1 + r2 <= r
then r in { (r22 + r12) where r22, r12 is Element of COMPLEX : ( r22 in X & r12 in Y ) } by MEMBER_1:def 6;
then consider r22, r12 being Element of COMPLEX such that
A5: r = r22 + r12 and
A6: r22 in X and
A7: r12 in Y ;
reconsider r9 = r22, r99 = r12 as real number by A6, A7;
A8: r2 <= r99 by A4, A7;
r1 <= r9 by A2, A6;
hence r1 + r2 <= r by A5, A8, XREAL_1:7; :: thesis: verum