let A, B be non empty Interval; :: thesis: for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.] & A misses B holds
not A \/ B is Interval
let p, q, r, s be R_eal; :: thesis: ( A = [.p,q.[ & B = ].r,s.] & A misses B implies not A \/ B is Interval )
assume that
A1: A = [.p,q.[ and
A2: B = ].r,s.] and
A3: A misses B ; :: thesis: A \/ B is not Interval
( p < q & r < s ) by A1, A2, XXREAL_1:26, XXREAL_1:27;
then A4: ( inf A = p & sup A = q & inf B = r & sup B = s ) by A1, A2, MEASURE6:11, MEASURE6:15, MEASURE6:9, MEASURE6:13;

per cases ( q <= r or s < p ) by A1, A2, A3, Th9;

suppose A5: q <= r ; :: thesis: A \/ B is not Interval

then A6: ( inf A < inf B & sup A < sup B ) by A4, A1, A2, XXREAL_1:26, XXREAL_1:27, XXREAL_0:2;
( not q in A & not q in B ) by A1, A2, A5, XXREAL_1:2, XXREAL_1:3;
then A7: not q in A \/ B by XBOOLE_0:def 3;
A8: ( inf A < q & q < sup B ) by A4, A5, A1, A2, XXREAL_1:26, XXREAL_1:27, XXREAL_0:2;

now :: thesis: A \/ B is not Interval

assume A9: A \/ B is Interval ; :: thesis: contradiction
( inf (A \/ B) = min ((inf A),(inf B)) & sup (A \/ B) = max ((sup A),(sup B)) ) by XXREAL_2:9, XXREAL_2:10;
then ( inf (A \/ B) = inf A & sup (A \/ B) = sup B ) by A6, XXREAL_0:def 9, XXREAL_0:def 10;
hence contradiction by A7, A8, A9, XXREAL_2:83; :: thesis: verum

end;

hence A \/ B is not Interval ; :: thesis: verum

end;

suppose A10: s < p ; :: thesis: A \/ B is not Interval

then A11: ( inf B < inf A & sup B < sup A ) by A4, A1, A2, XXREAL_1:26, XXREAL_1:27, XXREAL_0:2;
consider x being R_eal such that
A12: ( s < x & x < p & x in REAL ) by A10, MEASURE5:2;
( not x in A & not x in B ) by A1, A2, A12, XXREAL_1:2, XXREAL_1:3;
then A13: not x in A \/ B by XBOOLE_0:def 3;
A14: ( inf B < x & x < sup A ) by A12, A4, A1, A2, XXREAL_1:26, XXREAL_1:27, XXREAL_0:2;

now :: thesis: A \/ B is not Interval

assume A15: A \/ B is Interval ; :: thesis: contradiction
( inf (A \/ B) = min ((inf A),(inf B)) & sup (A \/ B) = max ((sup A),(sup B)) ) by XXREAL_2:9, XXREAL_2:10;
then ( inf (A \/ B) = inf B & sup (A \/ B) = sup A ) by A11, XXREAL_0:def 9, XXREAL_0:def 10;
hence contradiction by A13, A14, A15, XXREAL_2:83; :: thesis: verum

end;

hence A \/ B is not Interval ; :: thesis: verum

end;

end;