let r be real number ; :: thesis: ].r,+infty .] = ].r,+infty .[ \/ {+infty }
r in REAL by XREAL_0:def 1;
then r < +infty by XXREAL_0:9;
hence ].r,+infty .] = ].r,+infty .[ \/ {+infty } by Th132; :: thesis: verum