let p be Point of (Tunit_circle 2); :: thesis: p is not Point of (Topen_unit_circle p)
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 (Topen_unit_circle p) by A1, XBOOLE_0:def 5; :: thesis: verum