for p, q being Point of (Tunit_circle 2) st p <> q holds
q is Point of (Topen_unit_circle p)