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