reconsider r = r as Element of REAL by XREAL_0:def 1;
<*r*> in REAL 1 by FINSEQ_2:98;
hence |[r]| is Point of (TOP-REAL 1) by EUCLID:22; :: thesis: verum