let p be Point of (TOP-REAL 2); :: thesis: p = |[(proj1 . p),(proj2 . p)]|
( p = |[(p `1),(p `2)]| & p `1 = proj1 . p ) by EUCLID:53, PSCOMP_1:def 5;
hence p = |[(proj1 . p),(proj2 . p)]| by PSCOMP_1:def 6; :: thesis: verum