let x be Point of (TOP-REAL 2); :: thesis: ( x is Point of (Tunit_circle 2) & x `1 = 1 implies x `2 = 0 )
assume that
A1: x is Point of (Tunit_circle 2) and
A2: x `1 = 1 ; :: thesis: x `2 = 0
1 ^2 = |.x.| ^2 by A1, Th12
.= ((x `1) ^2) + ((x `2) ^2) by JGRAPH_3:1 ;
hence x `2 = 0 by A2; :: thesis: verum