theorem :: XXREAL_1:68

for p, q, r, s being ExtReal st p < q & ].p,q.] = ].r,s.] holds
( p = r & q = s )