let p, q, r, s be ExtReal; :: thesis: ( r < s implies ].r,s.[ <> ].p,q.] )
assume that
A1: r < s and
A2: ].r,s.[ = ].p,q.] ; :: thesis: contradiction
A3: not s in ].r,s.[ by Th4;
p <= r by A1, A2, Th59;
then A4: p < s by A1, XXREAL_0:2;
s <= q by A1, A2, Th59;
hence contradiction by A2, A3, A4, Th2; :: thesis: verum