for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & rseq is bounded holds
( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq )