let x be Point of (TOP-REAL 2); :: thesis: ( x is Point of (Tunit_circle 2) implies ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 ) )

assume A1: x is Point of (Tunit_circle 2) ; :: thesis: ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )

consider a, b being Element of REAL such that

A2: x = <*a,b*> by EUCLID:51;

A3: b = x `2 by A2, EUCLID:52;

A4: a = x `1 by A2, EUCLID:52;

A5: 1 ^2 = |.x.| ^2 by A1, Th12

.= (a ^2) + (b ^2) by A4, A3, JGRAPH_3:1 ;

0 <= a ^2 by XREAL_1:63;

then - (a ^2) <= - 0 ;

then A6: (b ^2) - 1 <= 0 by A5;

0 <= b ^2 by XREAL_1:63;

then - (b ^2) <= - 0 ;

then (a ^2) - 1 <= 0 by A5;

hence ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 ) by A4, A3, A6, SQUARE_1:43; :: thesis: verum

assume A1: x is Point of (Tunit_circle 2) ; :: thesis: ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )

consider a, b being Element of REAL such that

A2: x = <*a,b*> by EUCLID:51;

A3: b = x `2 by A2, EUCLID:52;

A4: a = x `1 by A2, EUCLID:52;

A5: 1 ^2 = |.x.| ^2 by A1, Th12

.= (a ^2) + (b ^2) by A4, A3, JGRAPH_3:1 ;

0 <= a ^2 by XREAL_1:63;

then - (a ^2) <= - 0 ;

then A6: (b ^2) - 1 <= 0 by A5;

0 <= b ^2 by XREAL_1:63;

then - (b ^2) <= - 0 ;

then (a ^2) - 1 <= 0 by A5;

hence ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 ) by A4, A3, A6, SQUARE_1:43; :: thesis: verum