let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies ['a,d'] \ ['b,c'] c= ['a,b'] \/ ['c,d'] )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: ['a,d'] \ ['b,c'] c= ['a,b'] \/ ['c,d']
then ADD: a < c by XXREAL_0:2;
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 ;
not x in ['b,c'] by XBOOLE_0:def 5, A2;
then A3: not x in [.b,c.] by INTEGRA5:def 3, A1;
x in ['a,d'] by XBOOLE_0:def 5, A2;
then x in [.a,d.] by INTEGRA5:def 3, ADD, XXREAL_0:2, A1;
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;
then x in ['a,b'] by INTEGRA5:def 3, A1;
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;
then x in ['c,d'] by INTEGRA5:def 3, A1;
hence x in ['a,b'] \/ ['c,d'] by XBOOLE_0:def 3; :: thesis: verum

end;

end;