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
A4: ( p < q & r < s ) by A1, A2, XXREAL_1:28;
then A5: ( inf A = p & sup A = q & inf B = r & sup B = s ) by A1, A2, MEASURE6:8, MEASURE6:12;

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

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

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

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, A4, A5, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
hence contradiction by A8, A5, A7, A4, 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

( not s in A & not s in B ) by A1, A2, A10, XXREAL_1:4;
then A11: not s in A \/ B by XBOOLE_0:def 3;
A12: ( inf B < s & s < sup A ) by A5, A10, A1, A2, XXREAL_1:28, XXREAL_0:2;

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

assume A13: 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 A10, A4, A5, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
hence contradiction by A11, A12, A13, XXREAL_2:83; :: thesis: verum

end;

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

end;

end;