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