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:40, XXREAL_1:44, XBOOLE_1:69;

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

then A /\ B = [.p,s.] by A1, A2, XXREAL_1:152;
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;

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

then A /\ B = ].r,q.[ by A1, A2, XXREAL_1:153;
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;