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