let p, q, r, s be ext-real number ; :: thesis: ( p < q & ].p,q.] = ].r,s.] implies ( p = r & q = s ) )
assume that
A1: p < q and
A2: ].p,q.] = ].r,s.] ; :: thesis: ( p = r & q = s )
A3: ( r <= p & q <= s ) by A1, A2, Th61;
then r < q by A1, XXREAL_0:2;
then r < s by A3, XXREAL_0:2;
then ( p <= r & s <= q ) by A2, Th61;
hence ( p = r & q = s ) by A3, XXREAL_0:1; :: thesis: verum