let p, q, r, s be ExtReal; ( p < q & ].p,q.[ = ].r,s.[ implies ( p = r & q = s ) )
assume that
A1:
p < q
and
A2:
].p,q.[ = ].r,s.[
; ( p = r & q = s )
A3:
r <= p
by A1, A2, Th63;
A4:
q <= s
by A1, A2, Th63;
r < q
by A1, A3, XXREAL_0:2;
then A5:
r < s
by A4, XXREAL_0:2;
then A6:
p <= r
by A2, Th63;
s <= q
by A2, A5, Th63;
hence
( p = r & q = s )
by A3, A4, A6, XXREAL_0:1; verum