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]

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

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

p is Point of (Tunit_circle 2)
by A1, PRE_TOPC:25;assume
p `1 = 1
; :: thesis: contradiction

then p = c[10] by A2, EUCLID:53;

hence contradiction by A1, Th21; :: thesis: verum

end;then p = c[10] by A2, EUCLID:53;

hence contradiction by A1, Th21; :: thesis: verum

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