theorem Th12: :: RINFSUP2:12

for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_above iff rseq is bounded_above )