set X = Topen_unit_circle p;

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

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] )
;

end;

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;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

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;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