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 Th320, A; :: thesis: verum