theorem Th4: :: SRINGS_5:4

for a, c being Real
for b being R_eal st a < b & [.a,b.[ c= [.a,c.[ holds
b is Real