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 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 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 implies C = Fr P )
assume that
A1: not BDD C is empty and
A2: U = P and
A3: U is a_component and
A4: C <> Fr P ; :: thesis: contradiction
A5: the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8;
reconsider T2C = (TOP-REAL 2) | (C `) as non empty SubSpace of TOP-REAL 2 ;
A6: T2C is locally_connected by JORDAN2C:81;
then U is open by A3, CONNSP_2:15;
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:22;
set Z = { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & X <> U ) } ;
set V = union { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & X <> U ) } ;
A8: ((union { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & 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 & X <> U ) } c= the carrier of (TOP-REAL 2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & 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 & 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 & X <> U ) } by TARSKI:def 4;
ex X being Subset of ((TOP-REAL 2) | (C `)) st
( X = A & X is a_component & 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 & 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 & 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 & X <> U ) } ) \/ U) \/ C
let a be object ; :: 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 & 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 & 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 & X <> U ) } ) \/ U) \/ C

hence a in ((union { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & 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 & X <> U ) } ) \/ U) \/ C

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

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 & X <> U ) } ) \/ U) \/ C

then a in (union { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & 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 & 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 & X <> U ) } ) \/ U) \/ C

Component_of a is a_component by CONNSP_1:40;
then Component_of a in { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & X <> U ) } by A14;
then a in union { X where X is Subset of ((TOP-REAL 2) | (C `)) : ( X is a_component & 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 & 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 & 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 object ; :: 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 & 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 & 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 & 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 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;
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:59;
A27: U <> {} ((TOP-REAL 2) | (C `)) by A3, CONNSP_1:32;

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 object 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:67;
then reconsider PC = P \/ C as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r being positive Real 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;
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;
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;
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:7;
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:28;
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:26;

now :: thesis: for x being object holds not x is_a_fixpoint_of F

let x be object ; :: 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 :: thesis: F . x <> x

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:5;
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:29;
A52: (DiskProj (p,r,p)) | (Sphere (p,r)) = id (Sphere (p,r)) by A44, Th65;
RotateCircle (p,r,p) is without_fixpoints by A44, Th67;
then A53: not x is_a_fixpoint_of RotateCircle (p,r,p) ;
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:12
.= (RotateCircle (p,r,p)) . ((DiskProj (p,r,p)) . (f . x)) by A33, A34, A49, A50, FUNCT_1:13
.= (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:49
.= (RotateCircle (p,r,p)) . x by A49, FUNCT_1:18 ;
hence F . x <> x by A32, A49, A53, A54; :: thesis: verum

end;

end;

end;

hence not x is_a_fixpoint_of F ; :: 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 ; :: thesis: verum

end;

end;

end;

then not F is with_fixpoint ;
hence contradiction by A45, BROUWER:14; :: thesis: verum

end;

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

consider p being object such that
A56: p in BDD C by A1;
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 and
U1 is bounded Subset of (Euclid 2) by A60, JORDAN2C:13;
U1 is open by A6, A62, CONNSP_2:15;
then reconsider P1 = P1 as non empty open bounded Subset of (TOP-REAL 2) by A57, A59, A60, A61, 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:67;
then reconsider PC = P1 \/ C as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider rv being positive Real such that
A65: PC c= Ball (p,rv) by A64, Th26;
not P c= Ball (p,rv) by A55, RLTOPSP1:42;
then consider u being object such that
A66: u in P and
A67: not u in Ball (p,rv) ;
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:35;
then p <> u by A57, A59, A66, XBOOLE_0:3;
then reconsider r = |.(u - p).| as non zero non negative Real by TOPRNS_1:28;
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;
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:28;
A72: C c= PC by XBOOLE_1:7;
then A73: C c= Ball (p,r) by A69;
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;
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:1;
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:7;
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:28;
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:26;

now :: thesis: for x being object holds not x is_a_fixpoint_of F

let x be object ; :: 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 :: thesis: F . x <> x

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:5;
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:18;
set SS = Sphere (p,r);
Sphere (p,r) c= C `

proof

let a be object ; :: 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:29;
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:8;
A95: u in SS by TOPREAL9:9;
SS is connected by CONNSP_1:23;
then ( SS misses U or SS c= U ) by A3, CONNSP_1:36;
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) is without_fixpoints by A85, Th67;
then A98: not x is_a_fixpoint_of RotateCircle (p,r,p) ;
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:12
.= (RotateCircle (p,r,p)) . ((DiskProj (p,r,p)) . (f . x)) by A75, A76, A90, A91, FUNCT_1:13
.= (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:49
.= (RotateCircle (p,r,p)) . x by A90, FUNCT_1:18 ;
hence F . x <> x by A74, A90, A98, A99; :: thesis: verum

end;

end;

end;

hence not x is_a_fixpoint_of F ; :: 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 ; :: thesis: verum

end;

end;

end;

then F is without_fixpoints ;
hence contradiction by A86, BROUWER:14; :: thesis: verum

end;

end;