let seq, seq1 be Real_Sequence; :: thesis: ( seq is bounded_below & seq1 is non-decreasing implies seq + seq1 is bounded_below )
assume that
A1: seq is bounded_below and
A2: seq1 is non-decreasing ; :: thesis: seq + seq1 is bounded_below
consider r1 being Real such that
A3: for n being Nat holds r1 < seq . n by A1;
take r = r1 + (seq1 . 0); :: according to SEQ_2:def 4 :: thesis: for b₁ being set holds not (seq + seq1) . b₁ <= r
let n be Nat; :: thesis: not (seq + seq1) . n <= r
seq1 . 0 <= seq1 . n by A2, Th11;
then r1 + (seq1 . 0) < (seq . n) + (seq1 . n) by A3, XREAL_1:8;
hence r < (seq + seq1) . n by SEQ_1:7; :: thesis: verum