let f be V8() standard special_circular_sequence; :: thesis: for P being Subset of (TOP-REAL 2)

for p being Point of (Euclid 2) 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 (TOP-REAL 2); :: thesis: for p being Point of (Euclid 2) 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 (Euclid 2); :: 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 (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: ( ((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 (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: (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 (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: ( 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 (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))

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

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: verum

for p being Point of (Euclid 2) 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 (TOP-REAL 2); :: thesis: for p being Point of (Euclid 2) 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 (Euclid 2); :: 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 (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: ( ((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 (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: (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 (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: ( 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 (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

A11:
L c= (L~ f) `
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 (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: verum

end;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 (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: verum

proof

L is connected
by JORDAN2C:53;
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 (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 ;

end;assume A12: l in L ; :: thesis: l in (L~ f) `

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: not l in L~ f

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

then dist (t,p) < ((dist (p,c)) + r) + 1 by A7, METRIC_1:11;

hence contradiction by A1, A13, TOPREAL6:25; :: thesis: verum

end;then dist (t,p) < ((dist (p,c)) + r) + 1 by A7, METRIC_1:11;

hence contradiction by A1, A13, TOPREAL6:25; :: thesis: verum

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

then A16:
M in { W where W is Subset of (TOP-REAL 2) : W is_outside_component_of L~ f }
;
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 M is bounded

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: verum

end;thus M is_a_component_of (L~ f) ` by A14; :: according to JORDAN2C:def 3 :: thesis: not M is bounded

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: verum

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: verum