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:29;
A5: ( inf A = p & sup A = q & inf B = r & sup B = s ) by A1, A2, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
per cases ( q < r or s < p ) by A1, A2, A3, Th4;
suppose A6: q < r ; :: thesis: A \/ B is not Interval
then consider x being R_eal such that
A7: ( q < x & x < r & x in REAL ) by MEASURE5:2;
( not x in A & not x in B ) by A1, A2, A7, XXREAL_1:1;
then A8: not x in A \/ B by XBOOLE_0:def 3;
A9: ( inf A < x & x < sup B ) by A7, A4, A5, XXREAL_0:2;
now :: thesis: A \/ B is not Interval
assume A10: 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, A9, A10, XXREAL_2:83; :: thesis: verum
end;
hence A \/ B is not Interval ; :: thesis: verum
end;
suppose A11: s < p ; :: thesis: A \/ B is not Interval
then consider x being R_eal such that
A12: ( s < x & x < p & x in REAL ) by MEASURE5:2;
( not x in A & not x in B ) by A1, A2, A12, XXREAL_1:1;
then A13: not x in A \/ B by XBOOLE_0:def 3;
A14: ( inf B < x & x < sup A ) by A12, A4, A5, 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, A4, A5, XXREAL_0:2, 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;