for x being object st x in ].r,+infty.[ holds
x in REAL by XREAL_0:def 1;
hence ].r,+infty.[ is Subset of REAL by TARSKI:def 3; :: thesis: verum