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 a < c by XXREAL_0:2;
then B1: [.a,d.] = ['a,d'] by INTEGRA5:def 3, XXREAL_0:2, A1;
B2: [.b,c.] = ['b,c'] by INTEGRA5:def 3, A1;
B3: [.a,b.] = ['a,b'] by INTEGRA5:def 3, A1;
[.c,d.] = ['c,d'] by INTEGRA5:def 3, A1;
hence [.a,d.] \ [.b,c.] c= [.a,b.] \/ [.c,d.] by B1, B2, B3, Th6, A1; :: thesis: verum