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