let p, q, r, s be ExtReal; :: 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 A3: [.r,s.] c= [.p,q.] ;
then A4: p <= r by A1, Th50;
A5: s <= q by A1, A3, Th50;
( p <> r or s <> q ) by A2;
hence ( p < r or s < q ) by A4, A5, XXREAL_0:1; :: thesis: verum