set X = Topen_unit_circle p;
A1: the carrier of (Topen_unit_circle p) = the carrier of (Tunit_circle 2) \ {p} by Def10;

per cases ( p = c[10] or p <> c[10] ) ;

suppose A2: p = c[10] ; :: thesis: not Topen_unit_circle p is empty

set x = |[0 ,1]|;
reconsider r = p as Point of (TOP-REAL 2) by PRE_TOPC:55;
A3: |[0 ,1]| `1 = 0 by EUCLID:56;
A4: |[0 ,1]| `2 = 1 by EUCLID:56;
|.(|[(0 + 0 ),(1 + 0 )]| - |[0 ,0 ]|).| = |.((|[0 ,1]| + |[0 ,0 ]|) - |[0 ,0 ]|).| by EUCLID:60
.= |.(|[0 ,1]| + (|[0 ,0 ]| - |[0 ,0 ]|)).| by EUCLID:49
.= |.(|[0 ,1]| + (0. (TOP-REAL 2))).| by EUCLID:46
.= |.|[0 ,1]|.| by EUCLID:31
.= sqrt ((1 ^2 ) + (0 ^2 )) by A3, A4, JGRAPH_1:47
.= 1 by SQUARE_1:89 ;
then A5: |[0 ,1]| in the carrier of (Tunit_circle 2) by Lm13;
r `1 = 1 by A2, EUCLID:56;
then not |[0 ,1]| in {p} by A3, TARSKI:def 1;
hence not the carrier of (Topen_unit_circle p) is empty by A1, A5, XBOOLE_0:def 5; :: according to STRUCT_0:def 1 :: thesis: verum

end;

suppose p <> c[10] ; :: thesis: not Topen_unit_circle p is empty

then not c[10] in {p} by TARSKI:def 1;
hence not the carrier of (Topen_unit_circle p) is empty by A1, XBOOLE_0:def 5; :: according to STRUCT_0:def 1 :: thesis: verum

end;

end;