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