let a, b, c, d be Real; :: thesis: [.a,d.] \ [.b,c.] c= [.a,b.[ \/ ].c,d.]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.a,d.] \ [.b,c.] or x in [.a,b.[ \/ ].c,d.] )
assume A2: x in [.a,d.] \ [.b,c.] ; :: thesis: x in [.a,b.[ \/ ].c,d.]
then reconsider x = x as Real ;
A3: not x in [.b,c.] by XBOOLE_0:def 5, A2;
x in [.a,d.] by XBOOLE_0:def 5, A2;
then A4: ( a <= x & x <= d ) by XXREAL_1:1;

per cases ( x < b or x > c ) by A3;

suppose x < b ; :: thesis: x in [.a,b.[ \/ ].c,d.]

then x in [.a,b.[ by A4;
hence x in [.a,b.[ \/ ].c,d.] by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x > c ; :: thesis: x in [.a,b.[ \/ ].c,d.]

then x in ].c,d.] by A4;
hence x in [.a,b.[ \/ ].c,d.] by XBOOLE_0:def 3; :: thesis: verum

end;

end;