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:25;
A3: |[0,1]| `1 = 0 by EUCLID:52;
A4: |[0,1]| `2 = 1 by EUCLID:52;
|.(|[(0 + 0),(1 + 0)]| - |[0,0]|).| = |.((|[0,1]| + |[0,0]|) - |[0,0]|).| by EUCLID:56
.= |.(|[0,1]| + (|[0,0]| - |[0,0]|)).| by RLVECT_1:def 3
.= |.(|[0,1]| + (0. (TOP-REAL 2))).| by RLVECT_1:5
.= |.|[0,1]|.| by RLVECT_1:4
.= sqrt ((1 ^2) + (0 ^2)) by A3, A4, JGRAPH_1:30
.= 1 by SQUARE_1:22 ;
then A5: |[0,1]| in the carrier of (Tunit_circle 2) by Lm13;
r `1 = 1 by A2, EUCLID:52;
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;