for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n = - (seq2 . n) ) holds
( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) )