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 & A \/ B is Interval & not ( p = s & A \/ B = ].r,q.] ) holds
( q = r & A \/ B = [.p,s.[ )
let p, q, r, s be R_eal; :: thesis: ( A = [.p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval & not ( p = s & A \/ B = ].r,q.] ) implies ( q = r & A \/ B = [.p,s.[ ) )
assume that
A1: A = [.p,q.] and
A2: B = ].r,s.[ and
A3: A misses B and
A4: A \/ B is Interval ; :: thesis: ( ( p = s & A \/ B = ].r,q.] ) or ( q = r & A \/ B = [.p,s.[ ) )
A5: ( p <= q & r < s ) by A1, A2, XXREAL_1:28, XXREAL_1:29;
then A6: ( inf A = p & sup A = q & inf B = r & sup B = s ) by A1, A2, MEASURE6:10, MEASURE6:14, MEASURE6:8, MEASURE6:12;

A7: now :: thesis: not q < r

assume A8: q < r ; :: thesis: contradiction
then consider x being R_eal such that
A9: ( q < x & x < r & x in REAL ) by MEASURE5:2;
( not x in A & not x in B ) by A1, A2, A9, XXREAL_1:1, XXREAL_1:4;
then A10: not x in A \/ B by XBOOLE_0:def 3;
( 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 A5, A6, A8, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
then ( inf (A \/ B) < x & x < sup (A \/ B) ) by A5, A6, A9, XXREAL_0:2;
hence contradiction by A10, A4, XXREAL_2:83; :: thesis: verum

end;

A11: now :: thesis: not s < p

assume A12: s < p ; :: thesis: contradiction
then consider x being R_eal such that
A13: ( s < x & x < p & x in REAL ) by MEASURE5:2;
( not x in A & not x in B ) by A1, A2, A13, XXREAL_1:1, XXREAL_1:4;
then A14: not x in A \/ B by XBOOLE_0:def 3;
( 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 A5, A6, A12, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
then ( inf (A \/ B) < x & x < sup (A \/ B) ) by A5, A6, A13, XXREAL_0:2;
hence contradiction by A14, A4, XXREAL_2:83; :: thesis: verum

end;

A15: ( q <= r or s <= p ) by A1, A2, A3, Th7;

per cases ( q = r or s = p ) by A15, A7, A11, XXREAL_0:1;

suppose q = r ; :: thesis: ( ( p = s & A \/ B = ].r,q.] ) or ( q = r & A \/ B = [.p,s.[ ) )

hence ( ( p = s & A \/ B = ].r,q.] ) or ( q = r & A \/ B = [.p,s.[ ) ) by A1, A2, A5, XXREAL_1:169; :: thesis: verum

end;

suppose A16: s = p ; :: thesis: ( ( p = s & A \/ B = ].r,q.] ) or ( q = r & A \/ B = [.p,s.[ ) )

A = {p} \/ ].p,q.] by A1, XXREAL_1:29, XXREAL_1:130;
then A \/ B = (].r,s.[ \/ {p}) \/ ].p,q.] by A2, XBOOLE_1:4;
then A \/ B = ].r,s.] \/ ].p,q.] by A16, A2, XXREAL_1:28, XXREAL_1:132;
hence ( ( p = s & A \/ B = ].r,q.] ) or ( q = r & A \/ B = [.p,s.[ ) ) by A5, A16, XXREAL_1:170; :: thesis: verum

end;

end;