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:37, XXREAL_1:47, XBOOLE_1:69;

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

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

end;

end;