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