theorem :: XXREAL_1:222

for p, q being ExtReal st p <= q holds
[.p,q.] = [.p,q.] \/ [.q,p.]