let seq be nonnegative ExtREAL_sequence; :: thesis: ( not seq is non-decreasing or seq is convergent_to_+infty or seq is convergent_to_finite_number )
assume A1: seq is non-decreasing ; :: thesis: ( seq is convergent_to_+infty or seq is convergent_to_finite_number )
now :: thesis: not seq is convergent_to_-infty
assume seq is convergent_to_-infty ; :: thesis: contradiction
then consider N being Nat such that
A4: for n being Nat st N <= n holds
seq . n <= - 1 by MESFUNC5:def 10;
( seq . N <= - 1 & seq . N >= 0 ) by SUPINF_2:51, A4;
hence contradiction ; :: thesis: verum
end;
hence ( seq is convergent_to_+infty or seq is convergent_to_finite_number ) by A1, RINFSUP2:37, MESFUNC5:def 11; :: thesis: verum