theorem :: XXREAL_1:428

for r being Real holds ].r,+infty.] = ].r,+infty.[ \/ {+infty}