let r, p be ext-real number ; :: thesis: [.r,+infty .] \ [.p,+infty .[ = [.r,p.[ \/ {+infty }
A1: r <= +infty by XXREAL_0:3;
p <= +infty by XXREAL_0:3;
hence [.r,+infty .] \ [.p,+infty .[ = [.r,p.[ \/ {+infty } by A1, Th320; :: thesis: verum