let p be Point of (TOP-REAL 3); :: thesis: p = |[(p `1),(p `2),(p `3)]|
ex x, y, z being Real st p = <*x,y,z*> by Th1;
hence p = |[(p `1),(p `2),(p `3)]| ; :: thesis: verum