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