theorem :: XXREAL_1:199

for p, q, r, s being ExtReal st ].p,q.] meets ].r,s.] holds
].p,q.] \ ].r,s.] = ].p,r.] \/ ].s,q.]