theorem Th11: :: RINFSUP2:11

for seq being ExtREAL_sequence st seq is bounded holds
seq is Real_Sequence