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 such that
A1: r1 is LowerBound of X ;
A2: for r being Real 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 such that
A3: r2 is LowerBound of Y ;
A4: for r being Real 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 ExtReal; :: 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 Complex : ( r22 in X & r12 in Y ) } by MEMBER_1:def 6;
then consider r22, r12 being Complex such that
A5: r = r22 + r12 and
A6: r22 in X and
A7: r12 in Y ;
reconsider r9 = r22, r99 = r12 as Real 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