theorem Th10: :: INTEGR23:8

for a, b, c, d being Real st b <= c holds
[.a,b.] /\ [.c,d.] c= [.b,b.]