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 r in ].r,s.[
by Th4;
A4:
p <= r
by A1, A2, Th51;
s <= q
by A1, A2, Th51;
then
r <= q
by A1, XXREAL_0:2;
hence
contradiction
by A2, A3, A4, Th1; verum