let f be constant standard special_circular_sequence; :: thesis:
let P be Subset of (TOP-REAL 2); :: thesis:
let p be Point of (Euclid 2); :: thesis:
assume that
A1: p = 0.REAL 2 and
A2: P is_outside_component_of L~ f ; :: thesis:
reconsider D = L~ f as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r being Real, c being Point of (Euclid 2) such that
A3: 0 < r and
c in D and
A4: for z being Point of (Euclid 2) st z in D holds
dist (c,z) <= r by TBSP_1:10;
set rr = ((dist (p,c)) + r) + 1;
take ((dist (p,c)) + r) + 1 ; :: thesis:
set L = (REAL 2) \ { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ;
((dist (p,c)) + r) + 0 < ((dist (p,c)) + r) + 1 by XREAL_1:8;
hence 0 < ((dist (p,c)) + r) + 1 by A3, METRIC_1:5, XREAL_1:8; :: thesis:
then ((dist (p,c)) + r) + 1 = |.(((dist (p,c)) + r) + 1).| by ABSVALUE:def 1;
then for a being Point of (TOP-REAL 2) holds
( a <> |[0,(((dist (p,c)) + r) + 1)]| or |.a.| >= ((dist (p,c)) + r) + 1 ) by TOPREAL6:23;
then not |[0,(((dist (p,c)) + r) + 1)]| in { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ;
then reconsider L = (REAL 2) \ { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } as non empty Subset of (TOP-REAL 2) by Lm1, XBOOLE_0:def 5;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: x in (Ball (p,(((dist (p,c)) + r) + 1))) ` ; :: thesis:
then reconsider y = x as Point of (Euclid 2) ;
reconsider z = y as Point of (TOP-REAL 2) by EUCLID:22;
A6: dist (p,y) = |.z.| by A1, TOPREAL6:25;
A7: D c= Ball (p,(((dist (p,c)) + r) + 1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A8: ((dist (p,c)) + r) + 0 < ((dist (p,c)) + r) + 1 by XREAL_1:6;
assume A9: x in D ; :: thesis:
then reconsider z = x as Point of (Euclid 2) ;
dist (c,z) <= r by A4, A9;
then A10: (dist (p,c)) + (dist (c,z)) <= (dist (p,c)) + r by XREAL_1:7;
dist (p,z) <= (dist (p,c)) + (dist (c,z)) by METRIC_1:4;
then dist (p,z) <= (dist (p,c)) + r by A10, XXREAL_0:2;
then dist (p,z) < ((dist (p,c)) + r) + 1 by A8, XXREAL_0:2;
hence x in Ball (p,(((dist (p,c)) + r) + 1)) by METRIC_1:11; :: thesis:

end;

A11: L c= (L~ f) `

proof

let l be object ; :: according to TARSKI:def 3 :: thesis:
assume A12: l in L ; :: thesis:
then reconsider j = l as Point of (TOP-REAL 2) ;
reconsider t = j as Point of (Euclid 2) by EUCLID:22;
not l in { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } by A12, XBOOLE_0:def 5;
then A13: |.j.| >= ((dist (p,c)) + r) + 1 ;

now :: thesis:

assume l in L~ f ; :: thesis:
then dist (t,p) < ((dist (p,c)) + r) + 1 by A7, METRIC_1:11;
hence contradiction by A1, A13, TOPREAL6:25; :: thesis:

end;

hence l in (L~ f) ` by A12, SUBSET_1:29; :: thesis:

end;

L is connected by JORDAN2C:53;
then consider M being Subset of (TOP-REAL 2) such that
A14: M is_a_component_of (L~ f) ` and
A15: L c= M by A11, GOBOARD9:3;
M is_outside_component_of L~ f

proof

reconsider W = L as Subset of (Euclid 2) ;
thus M is_a_component_of (L~ f) ` by A14; :: according to JORDAN2C:def 3 :: thesis:
not W is bounded by JORDAN2C:62;
then not L is bounded by JORDAN2C:11;
hence not M is bounded by A15, RLTOPSP1:42; :: thesis:

end;

then A16: M in { W where W is Subset of (TOP-REAL 2) : W is_outside_component_of L~ f } ;
not x in Ball (p,(((dist (p,c)) + r) + 1)) by A5, XBOOLE_0:def 5;
then for k being Point of (TOP-REAL 2) holds
( k <> z or |.k.| >= ((dist (p,c)) + r) + 1 ) by A6, METRIC_1:11;
then ( z in REAL 2 & not x in { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ) ;
then A17: x in L by XBOOLE_0:def 5;
UBD (L~ f) is_outside_component_of L~ f by JORDAN2C:68;
then P = UBD (L~ f) by A2, JORDAN2C:119;
hence x in P by A17, A15, A16, TARSKI:def 4; :: thesis: