let p be Point of ; :: thesis: p is not Point of
A1: p in {p} by TARSKI:def 1;
the carrier of (Topen_unit_circle p) = the carrier of (Tunit_circle 2) \ {p} by Def10;
hence p is not Point of by A1, XBOOLE_0:def 5; :: thesis: verum