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

let r9 be real number ; :: thesis: ( 0 < r9 implies ex r being real number st
( r in X + Y & r < ((lower_bound X) + (lower_bound Y)) + r9 ) )
assume 0 < r9 ; :: thesis: ex r being real number st
( r in X + Y & r < ((lower_bound X) + (lower_bound Y)) + r9 )
then A6: r9 / 2 > 0 by XREAL_1:217;
then consider r1 being real number such that
A7: r1 in X and
A8: r1 < (lower_bound X) + (r9 / 2) by A1, A2, SEQ_4:def 5;
consider r2 being real number such that
A9: r2 in Y and
A10: r2 < (lower_bound Y) + (r9 / 2) by A3, A4, A6, SEQ_4:def 5;
reconsider r = r1 + r2 as real number ;
take r = r; :: thesis: ( r in X + Y & r < ((lower_bound X) + (lower_bound Y)) + r9 )
thus r in X + Y by A7, A9; :: 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:10; :: thesis: verum

end;

A11: now

let r be real number ; :: 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 consider r1, r2 being Real such that
A12: r = r1 + r2 and
A13: ( r1 in X & r2 in Y ) ;
( r1 >= lower_bound X & r2 >= lower_bound Y ) by A2, A4, A13, SEQ_4:def 5;
hence (lower_bound X) + (lower_bound Y) <= r by A12, XREAL_1:9; :: thesis: verum

end;

( X + Y <> {} & X + Y is bounded_below ) by A1, A2, A3, A4, Th94, Th95;
hence lower_bound (X + Y) = (lower_bound X) + (lower_bound Y) by A11, A5, SEQ_4:def 5; :: thesis: verum