let X, Y be Subset of REAL; :: thesis: ( X <> {} & X is bounded_below & Y <> {} & Y is bounded_below implies lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y) )
assume that
A1: X <> {} and
A2: X is bounded_below and
A3: Y <> {} and
A4: Y is bounded_below ; :: thesis: lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)

A5: now :: thesis: for r9 being Real st 0 < r9 holds
ex r being Real st
( r in X ++ Y & r < ((lower_bound X) + (lower_bound Y)) + r9 )

let r9 be Real; :: thesis: ( 0 < r9 implies ex r being Real st
( r in X ++ Y & r < ((lower_bound X) + (lower_bound Y)) + r9 ) )
assume 0 < r9 ; :: thesis: ex r being Real st
( r in X ++ Y & r < ((lower_bound X) + (lower_bound Y)) + r9 )
then A6: r9 / 2 > 0 ;
then consider r1 being Real such that
A7: r1 in X and
A8: r1 < (lower_bound X) + (r9 / 2) by A1, A2, Def2;
consider r2 being Real such that
A9: r2 in Y and
A10: r2 < (lower_bound Y) + (r9 / 2) by A3, A4, A6, Def2;
reconsider r = r1 + r2 as Real ;
take r = r; :: thesis: ( r in X ++ Y & r < ((lower_bound X) + (lower_bound Y)) + r9 )
thus r in X ++ Y by A7, A9, MEMBER_1:46; :: thesis: r < ((lower_bound X) + (lower_bound Y)) + r9
((lower_bound X) + (r9 / 2)) + ((lower_bound Y) + (r9 / 2)) = ((lower_bound X) + (lower_bound Y)) + r9 ;
hence r < ((lower_bound X) + (lower_bound Y)) + r9 by A8, A10, XREAL_1:8; :: thesis: verum

end;

A11: now :: thesis: for r being Real st r in X ++ Y holds
(lower_bound X) + (lower_bound Y) <= r

let r be Real; :: thesis: ( r in X ++ Y implies (lower_bound X) + (lower_bound Y) <= r )
assume r in X ++ Y ; :: thesis: (lower_bound X) + (lower_bound Y) <= r
then r in { (r22 + r12) where r22, r12 is Complex : ( r22 in X & r12 in Y ) } by MEMBER_1:def 6;
then consider r11, r22 being Complex such that
A12: r = r11 + r22 and
A13: ( r11 in X & r22 in Y ) ;
reconsider r1 = r11, r2 = r22 as Real by A13;
( r1 >= lower_bound X & r2 >= lower_bound Y ) by A2, A4, A13, Def2;
hence (lower_bound X) + (lower_bound Y) <= r by A12, XREAL_1:7; :: thesis: verum

end;

( X ++ Y <> {} & X ++ Y is bounded_below ) by A1, A2, A3, A4, Th123;
hence lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y) by A11, A5, Def2; :: thesis: verum