reconsider x = x, y = y, z = z as Element of REAL by XREAL_0:def 1;
<*x,y,z*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
then <*x,y,z*> is Element of REAL 3 by EUCLID:def 1;
hence |[x,y,z]| is Point of (TOP-REAL 3) by EUCLID:22; :: thesis: verum