for x being set 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