theorem :: XXREAL_1:67

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