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:1 ;

hence x `1 = 0 by A2; :: thesis: verum

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:1 ;

hence x `1 = 0 by A2; :: thesis: verum