let seq be ExtREAL_sequence; :: thesis: ( seq is V116() implies not seq is convergent_to_-infty )
assume A1: seq is V116() ; :: thesis: not seq is convergent_to_-infty
assume seq is convergent_to_-infty ; :: thesis: contradiction
then consider n being Nat such that
A2: for m being Nat st n <= m holds
seq . m <= - 1 ;
seq . n <= - 1 by A2;
hence contradiction by A1, SUPINF_2:51; :: thesis: verum