let p, r be ExtReal; :: 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