theorem Th4: :: JORDAN5D:4

for r being Real
for g being FinSequence of REAL st r in rng g holds
( (Incr g) . 1 <= r & r <= (Incr g) . (len (Incr g)) )