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