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