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