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:46, XBOOLE_1:69;

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

then A /\ B = ].p,s.[ by A1, A2, XXREAL_1:160;
then ex x being object st x in A /\ B by A4, XXREAL_1:33, 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:160;
then ex x being object st x in A /\ B by A4, XXREAL_1:33, XBOOLE_0:def 1;
hence contradiction by A3, XBOOLE_0:4; :: thesis: verum

end;

end;