let f be V8() standard special_circular_sequence; :: thesis: for P being Subset of ()
for p being Point of () st p = 0.REAL 2 & P is_outside_component_of L~ f holds
ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P )

let P be Subset of (); :: thesis: for p being Point of () st p = 0.REAL 2 & P is_outside_component_of L~ f holds
ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P )

let p be Point of (); :: thesis: ( p = 0.REAL 2 & P is_outside_component_of L~ f implies ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P ) )

assume that
A1: p = 0.REAL 2 and
A2: P is_outside_component_of L~ f ; :: thesis: ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P )

reconsider D = L~ f as bounded Subset of () by JORDAN2C:11;
consider r being Real, c being Point of () such that
A3: 0 < r and
c in D and
A4: for z being Point of () 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: ( ((dist (p,c)) + r) + 1 > 0 & (Ball (p,(((dist (p,c)) + r) + 1))) ` c= P )
set L = (REAL 2) \ { a where a is Point of () : |.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 ; :: thesis: (Ball (p,(((dist (p,c)) + r) + 1))) ` c= P
then ((dist (p,c)) + r) + 1 = |.(((dist (p,c)) + r) + 1).| by ABSVALUE:def 1;
then for a being Point of () 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 () : |.a.| < ((dist (p,c)) + r) + 1 } ;
then reconsider L = (REAL 2) \ { a where a is Point of () : |.a.| < ((dist (p,c)) + r) + 1 } as non empty Subset of () by ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Ball (p,(((dist (p,c)) + r) + 1))) ` or x in P )
assume A5: x in (Ball (p,(((dist (p,c)) + r) + 1))) ` ; :: thesis: x in P
then reconsider y = x as Point of () ;
reconsider z = y as Point of () by EUCLID:22;
A6: dist (p,y) = |.z.| by ;
A7: D c= Ball (p,(((dist (p,c)) + r) + 1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in Ball (p,(((dist (p,c)) + r) + 1)) )
A8: ((dist (p,c)) + r) + 0 < ((dist (p,c)) + r) + 1 by XREAL_1:6;
assume A9: x in D ; :: thesis: x in Ball (p,(((dist (p,c)) + r) + 1))
then reconsider z = x as Point of () ;
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 ;
then dist (p,z) < ((dist (p,c)) + r) + 1 by ;
hence x in Ball (p,(((dist (p,c)) + r) + 1)) by METRIC_1:11; :: thesis: verum
end;
A11: L c= (L~ f) `
proof
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in L or l in (L~ f) ` )
assume A12: l in L ; :: thesis: l in (L~ f) `
then reconsider j = l as Point of () ;
reconsider t = j as Point of () by EUCLID:22;
not l in { a where a is Point of () : |.a.| < ((dist (p,c)) + r) + 1 } by ;
then A13: |.j.| >= ((dist (p,c)) + r) + 1 ;
now :: thesis: not l in L~ f
assume l in L~ f ; :: thesis: contradiction
then dist (t,p) < ((dist (p,c)) + r) + 1 by ;
hence contradiction by A1, A13, TOPREAL6:25; :: thesis: verum
end;
hence l in (L~ f) ` by ; :: thesis: verum
end;
L is connected by JORDAN2C:53;
then consider M being Subset of () such that
A14: M is_a_component_of (L~ f) ` and
A15: L c= M by ;
M is_outside_component_of L~ f
proof end;
then A16: M in { W where W is Subset of () : W is_outside_component_of L~ f } ;
not x in Ball (p,(((dist (p,c)) + r) + 1)) by ;
then for k being Point of () holds
( k <> z or |.k.| >= ((dist (p,c)) + r) + 1 ) by ;
then ( z in REAL 2 & not x in { a where a is Point of () : |.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 ;
hence x in P by ; :: thesis: verum