for seq being ExtREAL_sequence st lim_sup seq = lim_inf seq & lim_inf seq in REAL holds
ex k being Nat st seq ^\ k is bounded