let r, p be ext-real number ; :: thesis: [.r,+infty .] \ ].p,+infty .[ = [.r,p.] \/ {+infty }
A: ( r <= +infty & p <= +infty ) by XXREAL_0:3;
thus [.r,+infty .] \ ].p,+infty .[ = [.r,p.] \/ {+infty } by Th318, A; :: thesis: verum