let p be Point of (TOP-REAL 3); :: thesis: ex x, y, z being Real st p = <*x,y,z*>
the carrier of (TOP-REAL 3) = REAL 3 by EUCLID:22;
then p is Element of 3 -tuples_on REAL by EUCLID:def 1;
then p in 3 -tuples_on REAL ;
then reconsider p = p as Tuple of 3, REAL by FINSEQ_2:131;
ex x, y, z being Element of REAL st p = <*x,y,z*> by FINSEQ_2:103;
hence ex x, y, z being Real st p = <*x,y,z*> ; :: thesis: verum