theorem Th13: :: RINFSUP2:13

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