let X, Y be Subset of ; :: 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 r', r'' being Real such that
A3: r = r' + r'' and
A4: r' in X and
A5: r'' in Y ;
A6: r2 <= r'' by A2, A5;
r1 <= r' by A1, A4;
hence r1 + r2 <= r by A3, A6, XREAL_1:9; :: thesis: verum