let a, b, c, d be Real; :: thesis: ( a <= b & b < c & c <= d implies [.a,b.[ \/ ].c,d.] c= [.a,d.] \ [.b,c.] )
assume ( a <= b & b < c & c <= d ) ; :: thesis: [.a,b.[ \/ ].c,d.] c= [.a,d.] \ [.b,c.]
then ( a <= c & b <= d ) by XXREAL_0:2;
hence [.a,b.[ \/ ].c,d.] c= [.a,d.] \ [.b,c.] by XXREAL_1:312; :: thesis: verum