let p, q, r, s be Real; :: thesis: ( p < r & r <= s & s < q implies [.r,s.] c< [.p,q.] )
assume A1: ( p < r & r <= s & s < q ) ; :: thesis: [.r,s.] c< [.p,q.]
then r <= q by XXREAL_0:2;
then A3: p <= q by XXREAL_0:2, A1;
ex x being object st
( x in [.p,q.] & not x in [.r,s.] )

proof

take q ; :: thesis: ( q in [.p,q.] & not q in [.r,s.] )
thus ( q in [.p,q.] & not q in [.r,s.] ) by XXREAL_1:1, A1, A3; :: thesis: verum

end;

hence [.r,s.] c< [.p,q.] by XBOOLE_0:def 8, XXREAL_1:34, A1; :: thesis: verum