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: X + Y <> {} by A1, A3, Th94;
A6: X + Y is bounded_below by A2, A4, Th95;

A7: 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
A8: ( r = r1 + r2 & r1 in X & r2 in Y ) ;
A9: r1 >= lower_bound X by A2, A8, SEQ_4:def 5;
r2 >= lower_bound Y by A4, A8, SEQ_4:def 5;
hence (lower_bound X) + (lower_bound Y) <= r by A8, A9, XREAL_1:9; :: thesis: verum

end;

now

let r' be real number ; :: thesis: ( 0 < r' implies ex r being set st
( r in X + Y & r < ((lower_bound X) + (lower_bound Y)) + r' ) )
assume 0 < r' ; :: thesis: ex r being set st
( r in X + Y & r < ((lower_bound X) + (lower_bound Y)) + r' )
then A10: r' / 2 > 0 by XREAL_1:217;
then consider r1 being real number such that
A11: ( r1 in X & r1 < (lower_bound X) + (r' / 2) ) by A1, A2, SEQ_4:def 5;
consider r2 being real number such that
A12: ( r2 in Y & r2 < (lower_bound Y) + (r' / 2) ) by A3, A4, A10, SEQ_4:def 5;
take r = r1 + r2; :: thesis: ( r in X + Y & r < ((lower_bound X) + (lower_bound Y)) + r' )
thus r in X + Y by A11, A12; :: thesis: r < ((lower_bound X) + (lower_bound Y)) + r'
((lower_bound X) + (r' / 2)) + ((lower_bound Y) + (r' / 2)) = ((lower_bound X) + (lower_bound Y)) + r' ;
hence r < ((lower_bound X) + (lower_bound Y)) + r' by A11, A12, XREAL_1:10; :: thesis: verum

end;

hence lower_bound (X + Y) = (lower_bound X) + (lower_bound Y) by A5, A6, A7, SEQ_4:def 5; :: thesis: verum