for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) holds
( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )