theorem :: XXREAL_1:198

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