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

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