let A, B be non empty set ; :: thesis: for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.[ & A misses B & not q < r holds
s <= p
let p, q, r, s be R_eal; :: thesis: ( A = [.p,q.] & B = [.r,s.[ & A misses B & not q < r implies s <= p )
assume that
A1: A = [.p,q.] and
A2: B = [.r,s.[ and
A3: A misses B ; :: thesis: ( q < r or s <= p )
assume A4: ( q >= r & s > p ) ; :: thesis: contradiction

per cases ( ( r < p & s <= q ) or ( r >= p & s > q ) ) by A3, A1, A2, XXREAL_1:35, XXREAL_1:43, XBOOLE_1:69;

suppose ( r < p & s <= q ) ; :: thesis: contradiction

then A /\ B = [.p,s.[ by A1, A2, XXREAL_1:144;
then ex x being object st x in A /\ B by A4, XXREAL_1:31, XBOOLE_0:def 1;
hence contradiction by A3, XBOOLE_0:4; :: thesis: verum

end;

suppose ( r >= p & s > q ) ; :: thesis: contradiction

then A /\ B = [.r,q.] by A1, A2, XXREAL_1:145;
then ex x being object st x in A /\ B by A4, XXREAL_1:30, XBOOLE_0:def 1;
hence contradiction by A3, XBOOLE_0:4; :: thesis: verum

end;

end;