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 & REAL 3 = 3 -tuples_on REAL ) by EUCLID:25, EUCLID:def 1;
then reconsider p' = p as Element of 3 -tuples_on REAL ;
ex x, y, z being Real st p' = <*x,y,z*> by FINSEQ_2:123;
hence ex x, y, z being Real st p = <*x,y,z*> ; :: thesis: verum