theorem Th1: :: INTEGR19:1

for a, b, c being Real st a <= c & c <= b holds
( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )