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

now :: thesis: not r in ].p,q.[

assume r in ].p,q.[ ; :: thesis: contradiction
then A3: p < r by Th4;
s <= q by A1, A2, Th64;
then r < q by A1, XXREAL_0:2;
then p < q by A3, XXREAL_0:2;
hence contradiction by A2, A3, Th56; :: thesis: verum

end;

hence contradiction by A1, A2, Th3; :: thesis: verum