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

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

end;

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