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 holds
( p = s & A \/ B = ].r,q.[ )
let p, q, r, s be R_eal; :: thesis: ( A = [.p,q.[ & B = ].r,s.[ & A misses B & A \/ B is Interval implies ( p = s & A \/ B = ].r,q.[ ) )
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.[ )
A5: ( p < q & r < s ) by A1, A2, XXREAL_1:27, XXREAL_1:28;
then A6: ( inf A = p & sup A = q & inf B = r & sup B = s ) by A1, A2, MEASURE6:8, MEASURE6:11, MEASURE6:12, MEASURE6:15;

now :: thesis: not q <= r

assume A7: q <= r ; :: thesis: contradiction
then ( not q in A & not q in B ) by A1, A2, XXREAL_1:3, XXREAL_1:4;
then A8: not q in A \/ B by XBOOLE_0:def 3;
A9: ( inf A < inf B & sup A < sup B ) by A6, A7, A1, A2, XXREAL_1:27, XXREAL_1:28, XXREAL_0:2;
( 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) < q & q < sup (A \/ B) ) by A5, A6, A9, XXREAL_0:def 9, XXREAL_0:def 10;
hence contradiction by A8, A4, XXREAL_2:83; :: thesis: verum

end;

then A10: s <= p by A1, A2, A3, Th10;

now :: thesis: not s < p

assume A11: s < p ; :: thesis: contradiction
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:3, XXREAL_1:4;
then A13: not x in A \/ B by XBOOLE_0:def 3;
( min ((inf A),(inf B)) = inf B & max ((sup A),(sup B)) = sup A ) by A11, A6, A5, XXREAL_0:2, XXREAL_0:def 9, XXREAL_0:def 10;
then ( inf (A \/ B) = inf B & sup (A \/ B) = sup A ) by XXREAL_2:9, XXREAL_2:10;
then ( inf (A \/ B) < x & x < sup (A \/ B) ) by A6, A12, A1, A2, XXREAL_1:27, XXREAL_1:28, XXREAL_0:2;
hence contradiction by A13, A4, XXREAL_2:83; :: thesis: verum

end;

hence p = s by A10, XXREAL_0:1; :: thesis: A \/ B = ].r,q.[
hence A \/ B = ].r,q.[ by A1, A2, A5, XXREAL_1:173; :: thesis: verum