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 & a in P ` ) by A7, 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
A18: a in O and
A19: 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, A17, TARSKI:def 4, XBOOLE_0:3;
consider X being Subset of ((TOP-REAL 2) | (C ` )) such that
A20: X = O and
A21: X is_a_component_of (TOP-REAL 2) | (C ` ) and
A22: X <> U by A19;
Cl P misses X by A2, A3, A21, A22, Th68;
hence contradiction by A17, A18, A20, 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
A23: A is_an_arc_of p1,p2 and
A24: Fr P c= A and
A25: A c= C by BORSUK_4:84;
A26: 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
A27: p in U by A26, XBOOLE_0:def 1;
reconsider p = p as Point of (TOP-REAL 2) by A2, A27;
A28: 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
A29: PC c= Ball p,r by A28, Th26;
C c= PC by XBOOLE_1:7;
then A30: C c= Ball p,r by A29, XBOOLE_1:1;
set D = Tdisk p,r;
set S = Tcircle p,r;
set B = (cl_Ball p,r) \ {p};
A31: the carrier of (Tcircle p,r) = Sphere p,r by TOPREALB:9;
A32: the carrier of (Tdisk p,r) = cl_Ball p,r by BROUWER:3;
A33: Sphere p,r c= cl_Ball p,r by TOPREAL9:17;
A34: Ball p,r misses Sphere p,r by TOPREAL9:19;
A35: Ball p,r c= cl_Ball p,r by TOPREAL9:16;
A c= Ball p,r by A25, A30, XBOOLE_1:1;
then A is Subset of (Tdisk p,r) by A32, A35, XBOOLE_1:1;
then consider R being Function of (Tdisk p,r),((TOP-REAL 2) | A) such that
A36: R is continuous and
A37: R | A = id A by A23, Lm14;
P c= PC by XBOOLE_1:7;
then A38: P c= Ball p,r by A29, XBOOLE_1:1;
then consider f being Function of (Tdisk p,r),((TOP-REAL 2) | ((cl_Ball p,r) \ {p})) such that
A39: f is continuous and
A40: 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, A23, A24, A25, A27, A30, A36, A37, Lm15;
set g = DiskProj p,r,p;
set h = RotateCircle p,r,p;
A41: Tcircle p,r is SubSpace of Tdisk p,r by A31, A32, A33, TSEP_1:4;
reconsider F = (RotateCircle p,r,p) * ((DiskProj p,r,p) * f) as Function of (Tdisk p,r),(Tdisk p,r) by A31, A32, A33, FUNCT_2:9;
p is Point of (Tdisk p,r) by Th17;
then DiskProj p,r,p is continuous by Th64;
then A42: (DiskProj p,r,p) * f is continuous by A39;
|.(p - p).| = 0 by TOPRNS_1:29;
then A43: p in Ball p,r by TOPREAL9:7;
then RotateCircle p,r,p is continuous by Th66;
then (RotateCircle p,r,p) * ((DiskProj p,r,p) * f) is continuous by A42;
then A44: F is continuous by A41, 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 A45: x in dom F ; :: thesis: not b₁ is_a_fixpoint_of F

A46: (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 A32, A45, A46, XBOOLE_0:def 3;

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

F . x in the carrier of (Tcircle p,r) by A45, FUNCT_2:7;
hence F . x <> x by A31, A34, A47, XBOOLE_0:3; :: thesis: verum

end;

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

A49: dom f = the carrier of (Tdisk p,r) by FUNCT_2:def 1;
not x in P by A34, A38, A48, XBOOLE_0:3;
then A50: x in P ` by A48, SUBSET_1:50;
A51: (DiskProj p,r,p) | (Sphere p,r) = id (Sphere p,r) by A43, Th65;
RotateCircle p,r,p has_no_fixpoint by A43, Th67;
then A52: not x is_a_fixpoint_of RotateCircle p,r,p by ABIAN:def 5;
A53: 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 A45, FUNCT_1:22
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . (f . x)) by A32, A33, A48, A49, FUNCT_1:23
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . x) by A32, A33, A40, A48, A50
.= (RotateCircle p,r,p) . ((id (Sphere p,r)) . x) by A48, A51, FUNCT_1:72
.= (RotateCircle p,r,p) . x by A48, FUNCT_1:35 ;
hence F . x <> x by A31, A48, A52, A53, 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 A44, BROUWER:14; :: thesis: verum

end;

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

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

A86: (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 A73, A85, A86, XBOOLE_0:def 3;

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

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

end;

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

A89: dom f = the carrier of (Tdisk p,r) by FUNCT_2:def 1;
A90: 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 A91: a in Sphere p,r ; :: thesis: a in C `
assume not a in C ` ; :: thesis: contradiction
then A92: a in C by A91, SUBSET_1:50;
reconsider a = a as Point of (TOP-REAL 2) by A91;
a in PC by A70, A92;
then |.(a - p).| < rv by A63, TOPREAL9:7;
hence contradiction by A66, A91, TOPREAL9:9; :: thesis: verum

end;

then reconsider SS = Sphere p,r as Subset of ((TOP-REAL 2) | (C ` )) by PRE_TOPC:29;
A93: 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 A94: x in P by A2, A64, A88, A93, XBOOLE_0:3;
A95: (DiskProj p,r,p) | (Sphere p,r) = id (Sphere p,r) by A83, Th65;
RotateCircle p,r,p has_no_fixpoint by A83, Th67;
then A96: not x is_a_fixpoint_of RotateCircle p,r,p by ABIAN:def 5;
A97: 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 A85, FUNCT_1:22
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . (f . x)) by A73, A74, A88, A89, FUNCT_1:23
.= (RotateCircle p,r,p) . ((DiskProj p,r,p) . x) by A73, A74, A80, A88, A90, A94
.= (RotateCircle p,r,p) . ((id (Sphere p,r)) . x) by A88, A95, FUNCT_1:72
.= (RotateCircle p,r,p) . x by A88, FUNCT_1:35 ;
hence F . x <> x by A72, A88, A96, A97, 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 A84, BROUWER:14; :: thesis: verum

end;

end;