let C be Simple_closed_curve; :: thesis: for P being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C ` )) st not BDD C is empty & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) holds
C = Fr P
let P be Subset of (TOP-REAL 2); :: thesis: for U being Subset of ((TOP-REAL 2) | (C ` )) st not BDD C is empty & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) holds
C = Fr P
let U be Subset of ((TOP-REAL 2) | (C ` )); :: thesis: ( not BDD C is empty & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) implies C = Fr P )
assume that
A1: not BDD C is empty and
A2: U = P and
A3: U is_a_component_of (TOP-REAL 2) | (C ` ) and
A4: C <> Fr P ; :: thesis: contradiction
A5: the carrier of ((TOP-REAL 2) | (C ` )) = C ` by PRE_TOPC:29;
reconsider T2C = (TOP-REAL 2) | (C ` ) as non empty SubSpace of TOP-REAL 2 ;
A6: T2C is locally_connected by JORDAN2C:89;
then U is open by A3, CONNSP_2:21;
then reconsider P = P as open Subset of (TOP-REAL 2) by A2, TSEP_1:17;
A7: Fr P = (Cl P) /\ (P ` ) by PRE_TOPC:52;
set Z = { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ;
set V = union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ;
A8: ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C = the carrier of (TOP-REAL 2)

proof

A9: union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } or a in the carrier of (TOP-REAL 2) )
assume a in union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ; :: thesis: a in the carrier of (TOP-REAL 2)
then consider A being set such that
A10: a in A and
A11: A in { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } by TARSKI:def 4;
ex X being Subset of ((TOP-REAL 2) | (C ` )) st
( X = A & X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) by A11;
hence a in the carrier of (TOP-REAL 2) by A5, A10, TARSKI:def 3; :: thesis: verum

end;

U c= the carrier of (TOP-REAL 2) by A5, XBOOLE_1:1;
then (union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U c= the carrier of (TOP-REAL 2) by A9, XBOOLE_1:8;
hence ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C c= the carrier of (TOP-REAL 2) by XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (TOP-REAL 2) c= ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (TOP-REAL 2) or a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C )
assume A12: a in the carrier of (TOP-REAL 2) ; :: thesis: a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C

per cases ( a in C or not a in C ) ;

suppose a in C ; :: thesis: a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C

hence a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not a in C ; :: thesis: a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C

then reconsider a = a as Point of ((TOP-REAL 2) | (C ` )) by A5, A12, SUBSET_1:50;
A13: a in Component_of a by CONNSP_1:40;

per cases ( Component_of a = U or Component_of a <> U ) ;

suppose Component_of a = U ; :: thesis: a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C

then a in (union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U by A13, XBOOLE_0:def 3;
hence a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A14: Component_of a <> U ; :: thesis: a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C

Component_of a is_a_component_of (TOP-REAL 2) | (C ` ) by CONNSP_1:43;
then Component_of a in { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } by A14;
then a in union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } by A13, TARSKI:def 4;
then a in (union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U by XBOOLE_0:def 3;
hence a in ((union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U) \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

end;

A15: P misses P ` by XBOOLE_1:79;
Fr P c= C

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Fr P or a in C )
assume A16: a in Fr P ; :: thesis: a in C
then A17: a in Cl P by XBOOLE_0:def 4;
A18: a in P ` by A7, A16, XBOOLE_0:def 4;
assume not a in C ; :: thesis: contradiction
then a in (union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } ) \/ U by A8, A16, XBOOLE_0:def 3;
then ( a in union { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } or a in U ) by XBOOLE_0:def 3;
then consider O being set such that
A19: a in O and
A20: O in { X where X is Subset of ((TOP-REAL 2) | (C ` )) : ( X is_a_component_of (TOP-REAL 2) | (C ` ) & X <> U ) } by A2, A15, A18, TARSKI:def 4, XBOOLE_0:3;
consider X being Subset of ((TOP-REAL 2) | (C ` )) such that
A21: X = O and
A22: X is_a_component_of (TOP-REAL 2) | (C ` ) and
A23: X <> U by A20;
Cl P misses X by A2, A3, A22, A23, Th68;
hence contradiction by A17, A19, A21, XBOOLE_0:3; :: thesis: verum

end;

then Fr P c< C by A4, XBOOLE_0:def 8;
then consider p1, p2 being Point of (TOP-REAL 2), A being Subset of (TOP-REAL 2) such that
A24: A is_an_arc_of p1,p2 and
A25: Fr P c= A and
A26: A c= C by BORSUK_4:84;
A27: U <> {} ((TOP-REAL 2) | (C ` )) by A3, CONNSP_1:34;

per cases ( P is Bounded or not P is Bounded ) ;

suppose P is Bounded ; :: thesis: contradiction

then reconsider P = P as Bounded Subset of (TOP-REAL 2) ;
consider p being set such that
A28: p in U by A27, XBOOLE_0:def 1;
reconsider p = p as Point of (TOP-REAL 2) by A2, A28;
A29: P \/ C is Bounded by TOPREAL6:76;
then reconsider PC = P \/ C as bounded Subset of (Euclid 2) by JORDAN2C:def 2;
consider r being positive real number such that
A30: PC c= Ball p,r by A29, Th26;
C c= PC by XBOOLE_1:7;
then A31: C c= Ball p,r by A30, XBOOLE_1:1;
set D = Tdisk p,r;
set S = Tcircle p,r;
set B = (cl_Ball p,r) \ {p};
A32: the carrier of (Tcircle p,r) = Sphere p,r by TOPREALB:9;
A33: the carrier of (Tdisk p,r) = cl_Ball p,r by BROUWER:3;
A34: Sphere p,r c= cl_Ball p,r by TOPREAL9:17;
A35: Ball p,r misses Sphere p,r by TOPREAL9:19;
A36: Ball p,r c= cl_Ball p,r by TOPREAL9:16;
A c= Ball p,r by A26, A31, XBOOLE_1:1;
then A is Subset of (Tdisk p,r) by A33, A36, XBOOLE_1:1;
then consider R being Function of (Tdisk p,r),((TOP-REAL 2) | A) such that
A37: R is continuous and
A38: R | A = id A by A24, Lm12;
P c= PC by XBOOLE_1:7;
then A39: P c= Ball p,r by A30, XBOOLE_1:1;
then consider f being Function of (Tdisk p,r),((TOP-REAL 2) | ((cl_Ball p,r) \ {p})) such that
A40: f is continuous and
A41: for x being Point of (Tdisk p,r) holds
( ( x in Cl P implies f . x = R . x ) & ( x in P ` implies f . x = x ) ) by A2, A3, A7, A24, A25, A26, A28, A31, A37, A38, Lm13;
set g = DiskProj p,r,p;
set h = RotateCircle p,r,p;
A42: Tcircle p,r is SubSpace of Tdisk p,r by A32, A33, A34, TSEP_1:4;
reconsider F = (RotateCircle p,r,p) * ((DiskProj p,r,p) * f) as Function of (Tdisk p,r),(Tdisk p,r) by A32, A33, A34, FUNCT_2:9;
p is Point of (Tdisk p,r) by Th17;
then A43: DiskProj p,r,p is continuous by Th64;
|.(p - p).| = 0 by TOPRNS_1:29;
then A44: p in Ball p,r by TOPREAL9:7;
then RotateCircle p,r,p is continuous by Th66;
then A45: F is continuous by A40, A42, A43, PRE_TOPC:56;

now

let x be set ; :: thesis: not b₁ is_a_fixpoint_of F

per cases ( x in dom F or not x in dom F ) ;

suppose A46: x in dom F ; :: thesis: not b₁ is_a_fixpoint_of F

A47: (Ball p,r) \/ (Sphere p,r) = cl_Ball p,r by TOPREAL9:18;

now

per cases ( x in Ball p,r or x in Sphere p,r ) by A33, A46, A47, XBOOLE_0:def 3;

suppose A48: x in Ball p,r ; :: thesis: F . x <> x

F . x in the carrier of (Tcircle p,r) by A46, FUNCT_2:7;
hence F . x <> x by A32, A35, A48, XBOOLE_0:3; :: thesis: verum

end;

suppose A49: x in Sphere p,r ; :: thesis: F . x <> x

A50: dom f = the carrier of (Tdisk p,r) by FUNCT_2:def 1;
not x in P by A35, A39, A49, XBOOLE_0:3;
then A51: x in P ` by A49, SUBSET_1:50;
A52: (DiskProj p,r,p) | (Sphere p,r) = id (Sphere p,r) by A44, Th65;
RotateCircle p,r,p has_no_fixpoint by A44, Th67;
then A53: not x is_a_fixpoint_of RotateCircle p,r,p by ABIAN:def 5;
A54: dom (RotateCircle p,r,p) = the carrier of (Tcircle p,r) by FUNCT_2:def 1;
F . x = (RotateCircle p,r,p) . (((DiskProj p,r,p) * f) . x) by A46, FUNCT_1:22
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . (f . x)) by A33, A34, A49, A50, FUNCT_1:23
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . x) by A33, A34, A41, A49, A51
.= (RotateCircle p,r,p) . ((id (Sphere p,r)) . x) by A49, A52, FUNCT_1:72
.= (RotateCircle p,r,p) . x by A49, FUNCT_1:35 ;
hence F . x <> x by A32, A49, A53, A54, ABIAN:def 3; :: thesis: verum

end;

end;

end;

hence not x is_a_fixpoint_of F by ABIAN:def 3; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: not b₁ is_a_fixpoint_of F

hence not x is_a_fixpoint_of F by ABIAN:def 3; :: thesis: verum

end;

end;

end;

then not F has_a_fixpoint by ABIAN:def 5;
hence contradiction by A45, BROUWER:14; :: thesis: verum

end;

suppose A55: not P is Bounded ; :: thesis: contradiction

consider p being set such that
A56: p in BDD C by A1, XBOOLE_0:def 1;
consider Z being set such that
A57: p in Z and
A58: Z in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by A56, TARSKI:def 4;
consider P1 being Subset of (TOP-REAL 2) such that
A59: Z = P1 and
A60: P1 is_inside_component_of C by A58;
consider U1 being Subset of ((TOP-REAL 2) | (C ` )) such that
A61: U1 = P1 and
A62: U1 is_a_component_of (TOP-REAL 2) | (C ` ) and
U1 is bounded Subset of (Euclid 2) by A60, JORDAN2C:17;
U1 is open by A6, A62, CONNSP_2:21;
then reconsider P1 = P1 as non empty open Bounded Subset of (TOP-REAL 2) by A57, A59, A60, A61, JORDAN2C:def 3, TSEP_1:17;
reconsider p = p as Point of (TOP-REAL 2) by A57, A59;
A63: p in P1 by A57, A59;
A64: P1 \/ C is Bounded by TOPREAL6:76;
then reconsider PC = P1 \/ C as bounded Subset of (Euclid 2) by JORDAN2C:def 2;
consider rv being positive real number such that
A65: PC c= Ball p,rv by A64, Th26;
not P c= Ball p,rv by A55, JORDAN2C:16;
then consider u being set such that
A66: u in P and
A67: not u in Ball p,rv by TARSKI:def 3;
reconsider u = u as Point of (TOP-REAL 2) by A66;
set r = |.(u - p).|;
P misses P1 by A2, A3, A55, A61, A62, CONNSP_1:37;
then p <> u by A57, A59, A66, XBOOLE_0:3;
then reconsider r = |.(u - p).| as non empty non negative real number by TOPRNS_1:29;
A68: r >= rv by A67, TOPREAL9:7;
then Ball p,rv c= Ball p,r by Th18;
then A69: PC c= Ball p,r by A65, XBOOLE_1:1;
A70: Fr (Ball p,r) = Sphere p,r by Th24;
u in Sphere p,r by TOPREAL9:9;
then A71: P meets Ball p,r by A66, A70, TOPS_1:61;
A72: C c= PC by XBOOLE_1:7;
then A73: C c= Ball p,r by A69, XBOOLE_1:1;
set D = Tdisk p,r;
set S = Tcircle p,r;
set B = (cl_Ball p,r) \ {p};
A74: the carrier of (Tcircle p,r) = Sphere p,r by TOPREALB:9;
A75: the carrier of (Tdisk p,r) = cl_Ball p,r by BROUWER:3;
A76: Sphere p,r c= cl_Ball p,r by TOPREAL9:17;
A77: Ball p,r misses Sphere p,r by TOPREAL9:19;
A78: Ball p,r c= cl_Ball p,r by TOPREAL9:16;
A c= Ball p,r by A26, A73, XBOOLE_1:1;
then A is Subset of (Tdisk p,r) by A75, A78, XBOOLE_1:1;
then consider R being Function of (Tdisk p,r),((TOP-REAL 2) | A) such that
A79: R is continuous and
A80: R | A = id A by A24, Lm12;
p1 in A by A24, TOPREAL1:4;
then consider f being Function of (Tdisk p,r),((TOP-REAL 2) | ((cl_Ball p,r) \ {p})) such that
A81: f is continuous and
A82: for x being Point of (Tdisk p,r) holds
( ( x in Cl P implies f . x = x ) & ( x in P ` implies f . x = R . x ) ) by A2, A3, A7, A25, A26, A55, A61, A62, A63, A71, A73, A79, A80, Lm14;
set g = DiskProj p,r,p;
set h = RotateCircle p,r,p;
A83: Tcircle p,r is SubSpace of Tdisk p,r by A74, A75, A76, TSEP_1:4;
reconsider F = (RotateCircle p,r,p) * ((DiskProj p,r,p) * f) as Function of (Tdisk p,r),(Tdisk p,r) by A74, A75, A76, FUNCT_2:9;
p is Point of (Tdisk p,r) by Th17;
then A84: DiskProj p,r,p is continuous by Th64;
|.(p - p).| = 0 by TOPRNS_1:29;
then A85: p in Ball p,r by TOPREAL9:7;
then RotateCircle p,r,p is continuous by Th66;
then A86: F is continuous by A81, A83, A84, PRE_TOPC:56;

now

let x be set ; :: thesis: not b₁ is_a_fixpoint_of F

per cases ( x in dom F or not x in dom F ) ;

suppose A87: x in dom F ; :: thesis: not b₁ is_a_fixpoint_of F

A88: (Ball p,r) \/ (Sphere p,r) = cl_Ball p,r by TOPREAL9:18;

now

per cases ( x in Ball p,r or x in Sphere p,r ) by A75, A87, A88, XBOOLE_0:def 3;

suppose A89: x in Ball p,r ; :: thesis: F . x <> x

F . x in the carrier of (Tcircle p,r) by A87, FUNCT_2:7;
hence F . x <> x by A74, A77, A89, XBOOLE_0:3; :: thesis: verum

end;

suppose A90: x in Sphere p,r ; :: thesis: F . x <> x

A91: dom f = the carrier of (Tdisk p,r) by FUNCT_2:def 1;
A92: P c= Cl P by PRE_TOPC:48;
set SS = Sphere p,r;
Sphere p,r c= C `

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Sphere p,r or a in C ` )
assume A93: a in Sphere p,r ; :: thesis: a in C `
assume not a in C ` ; :: thesis: contradiction
then A94: a in C by A93, SUBSET_1:50;
reconsider a = a as Point of (TOP-REAL 2) by A93;
a in PC by A72, A94;
then |.(a - p).| < rv by A65, TOPREAL9:7;
hence contradiction by A68, A93, TOPREAL9:9; :: thesis: verum

end;

then reconsider SS = Sphere p,r as Subset of ((TOP-REAL 2) | (C ` )) by PRE_TOPC:29;
A95: u in SS by TOPREAL9:9;
SS is connected by CONNSP_1:24;
then ( SS misses U or SS c= U ) by A3, CONNSP_1:38;
then A96: x in P by A2, A66, A90, A95, XBOOLE_0:3;
A97: (DiskProj p,r,p) | (Sphere p,r) = id (Sphere p,r) by A85, Th65;
RotateCircle p,r,p has_no_fixpoint by A85, Th67;
then A98: not x is_a_fixpoint_of RotateCircle p,r,p by ABIAN:def 5;
A99: dom (RotateCircle p,r,p) = the carrier of (Tcircle p,r) by FUNCT_2:def 1;
F . x = (RotateCircle p,r,p) . (((DiskProj p,r,p) * f) . x) by A87, FUNCT_1:22
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . (f . x)) by A75, A76, A90, A91, FUNCT_1:23
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . x) by A75, A76, A82, A90, A92, A96
.= (RotateCircle p,r,p) . ((id (Sphere p,r)) . x) by A90, A97, FUNCT_1:72
.= (RotateCircle p,r,p) . x by A90, FUNCT_1:35 ;
hence F . x <> x by A74, A90, A98, A99, ABIAN:def 3; :: thesis: verum

end;

end;

end;

hence not x is_a_fixpoint_of F by ABIAN:def 3; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: not b₁ is_a_fixpoint_of F

hence not x is_a_fixpoint_of F by ABIAN:def 3; :: thesis: verum

end;

end;

end;

then not F has_a_fixpoint by ABIAN:def 5;
hence contradiction by A86, BROUWER:14; :: thesis: verum

end;

end;