theorem Th24: :: RINFSUP2:24

for seq being ExtREAL_sequence holds inf seq <= sup seq