for seq being ExtREAL_sequence
for n being Nat holds { (seq . k) where k is Nat : n <= k } is non empty Subset of ExtREAL