let r, s, p, q be ext-real number ; :: thesis: ( r <= s & [.r,s.] c< [.p,q.] & not p < r implies s < q )
assume A1: r <= s ; :: thesis: ( not [.r,s.] c< [.p,q.] or p < r or s < q )
assume A2: [.r,s.] c< [.p,q.] ; :: thesis: ( p < r or s < q )
then [.r,s.] c= [.p,q.] by XBOOLE_0:def 8;
then A3: ( p <= r & s <= q ) by A1, Th50;
( p <> r or s <> q ) by A2;
hence ( p < r or s < q ) by A3, XXREAL_0:1; :: thesis: verum