let r be Real; :: 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