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

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

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