theorem Th39: :: MEASURE6:39

for seq being Real_Sequence holds
( rng seq is real-bounded iff seq is bounded )