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