theorem Th4: :: RCOMP_1:4

for s, g being Real
for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
s1 is bounded