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