let p be Point of (TOP-REAL 2); :: thesis: ( p is Point of (Topen_unit_circle c[-10]) & p `2 = 0 implies p = c[10] )
assume that
A1: p is Point of (Topen_unit_circle c[-10]) and
A2: p `2 = 0 ; :: thesis: p = c[10]

A3: now :: thesis: not p `1 = - 1

assume p `1 = - 1 ; :: thesis: contradiction
then p = c[-10] by A2, EUCLID:53;
hence contradiction by A1, Th21; :: thesis: verum

end;

p is Point of (Tunit_circle 2) by A1, PRE_TOPC:25;
then 1 ^2 = |.p.| ^2 by Th12
.= ((p `1) ^2) + ((p `2) ^2) by JGRAPH_3:1 ;
then ( p `1 = 1 or p `1 = - 1 ) by A2, SQUARE_1:41;
hence p = c[10] by A2, A3, EUCLID:53; :: thesis: verum