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 A1: A = the carrier of (Topen_unit_circle p) ; :: thesis: A is open
A2: Tunit_circle 2 is T_2 by TOPMETR:3;
A ` = the carrier of (Tunit_circle 2) \ (the carrier of (Tunit_circle 2) \ {p}) by A1, Def10
.= the carrier of (Tunit_circle 2) /\ {p} by XBOOLE_1:48
.= {p} by ZFMISC_1:52 ;
then A ` is closed by A2, PCOMPS_1:10;
hence A is open by TOPS_1:30; :: thesis: verum