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