let seq be Real_Sequence; :: thesis: ( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) )
thus ( seq is non-decreasing implies seq is bounded_below ) :: thesis: ( seq is non-increasing implies seq is bounded_above )
proof
assume A1: seq is non-decreasing ; :: thesis: seq is bounded_below
take (seq . 0) - 1 ; :: according to SEQ_2:def 4 :: thesis: for b1 being set holds not seq . b1 <= (seq . 0) - 1
let n be Nat; :: thesis: not seq . n <= (seq . 0) - 1
( (seq . 0) - 1 < (seq . 0) - 0 & seq . 0 <= seq . n ) by A1, SEQM_3:11, XREAL_1:15;
hence not seq . n <= (seq . 0) - 1 by XXREAL_0:2; :: thesis: verum
end;
assume A2: seq is non-increasing ; :: thesis: seq is bounded_above
take (seq . 0) + 1 ; :: according to SEQ_2:def 3 :: thesis: for b1 being set holds not (seq . 0) + 1 <= seq . b1
let n be Nat; :: thesis: not (seq . 0) + 1 <= seq . n
( (seq . 0) + 0 < (seq . 0) + 1 & seq . n <= seq . 0 ) by A2, SEQM_3:12, XREAL_1:8;
hence not (seq . 0) + 1 <= seq . n by XXREAL_0:2; :: thesis: verum