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