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