let p be ExtReal; for r being Real holds ].r,+infty.] \ ].p,+infty.[ = ].r,p.] \/ {+infty}
let r be Real; ].r,+infty.] \ ].p,+infty.[ = ].r,p.] \/ {+infty}
r in REAL
by XREAL_0:def 1;
then
r < +infty
by XXREAL_0:9;
hence
].r,+infty.] \ ].p,+infty.[ = ].r,p.] \/ {+infty}
by Th317, XXREAL_0:3; verum