let A be Subset of (Tunit_circle 2); :: according to TSEP_1:def 1 :: thesis: ( not A = the carrier of (Topen_unit_circle p) or A is open )
assume A = the carrier of (Topen_unit_circle p) ; :: thesis: A is open
then A1: A ` = the carrier of (Tunit_circle 2) \ ( the carrier of (Tunit_circle 2) \ {p}) by Def10
.= the carrier of (Tunit_circle 2) /\ {p} by XBOOLE_1:48
.= {p} by ZFMISC_1:46 ;
Tunit_circle 2 is T_2 by TOPMETR:2;
then A ` is closed by A1, PCOMPS_1:7;
hence A is open by TOPS_1:4; :: thesis: verum