theorem :: XXREAL_1:26

for p, q being ExtReal st p <= q holds
].q,p.] = {}