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
B1: r1 is LowerBound of X by XXREAL_2:def 9;
A1: for r being real number st r in X holds
r1 <= r by B1, XXREAL_2:def 2;
assume Y is bounded_below ; :: thesis: X ++ Y is bounded_below
then consider r2 being real number such that
B2: r2 is LowerBound of Y by XXREAL_2:def 9;
A2: for r being real number st r in Y holds
r2 <= r by B2, 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
A3: r = r22 + r12 and
A4: r22 in X and
A5: r12 in Y ;
reconsider r9 = r22, r99 = r12 as real number by A4, A5;
A6: r2 <= r99 by A2, A5;
r1 <= r9 by A1, A4;
hence r1 + r2 <= r by A3, A6, XREAL_1:9; :: thesis: verum