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

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