let p, q be Point of ; :: thesis: ( p <> q implies q is Point of )
assume A1: p <> q ; :: thesis: q is Point of
the carrier of (Topen_unit_circle p) = the carrier of (Tunit_circle 2) \ {p} by Def10;
hence q is Point of by A1, ZFMISC_1:64; :: thesis: verum