for x being Point of (TOP-REAL 2) st x is Point of (Topen_unit_circle c[10]) holds
( - 1 <= x `1 & x `1 < 1 )