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
A1: for r being real number st r in X holds
r1 <= r by SEQ_4:def 2;
assume Y is bounded_below ; :: thesis: X + Y is bounded_below
then consider r2 being real number such that
A2: for r being real number st r in Y holds
r2 <= r by SEQ_4:def 2;
take r1 + r2 ; :: according to SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in X + Y or r1 + r2 <= b₁ )
let r be real number ; :: thesis: ( not r in X + Y or r1 + r2 <= r )
assume r in X + Y ; :: thesis: r1 + r2 <= r
then consider r9, r99 being Real such that
A3: r = r9 + r99 and
A4: r9 in X and
A5: r99 in Y ;
A6: r2 <= r99 by A2, A5;
r1 <= r9 by A1, A4;
hence r1 + r2 <= r by A3, A6, XREAL_1:9; :: thesis: verum