theorem :: XXREAL_1:155

for p, q, r, s being ExtReal st r >= p & s >= q holds
].r,s.[ /\ [.p,q.[ = ].r,q.[