let M be non empty compact locally_euclidean TopSpace; :: thesis: for C being Subset of M st C is a_component holds
( C is open & ex n being Nat st M | C is non empty b2 -locally_euclidean TopSpace )

defpred S1[ Point of M, Subset of M] means ( \$2 is a_neighborhood of \$1 & ex n being Nat st M | \$2, Tdisk ((0. ()),1) are_homeomorphic );
let C be Subset of M; :: thesis: ( C is a_component implies ( C is open & ex n being Nat st M | C is non empty b1 -locally_euclidean TopSpace ) )
assume A1: C is a_component ; :: thesis: ( C is open & ex n being Nat st M | C is non empty b1 -locally_euclidean TopSpace )
consider p being object such that
A2: p in C by ;
reconsider p = p as Point of M by A2;
A3: for x being Point of M ex y being Element of bool the carrier of M st S1[x,y]
proof
let x be Point of M; :: thesis: ex y being Element of bool the carrier of M st S1[x,y]
ex U being a_neighborhood of x ex n being Nat st M | U, Tdisk ((0. ()),1) are_homeomorphic by Def2;
hence ex y being Element of bool the carrier of M st S1[x,y] ; :: thesis: verum
end;
consider W being Function of M,(bool the carrier of M) such that
A4: for x being Point of M holds S1[x,W . x] from reconsider MC = M | C as non empty connected TopSpace by ;
defpred S2[ object , object ] means ( \$2 in C & ( for A being Subset of M st A = W . \$2 holds
Int A = \$1 ) );
set IntW = { (Int U) where U is Subset of M : U in rng (W | C) } ;
{ (Int U) where U is Subset of M : U in rng (W | C) } c= bool the carrier of M
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Int U) where U is Subset of M : U in rng (W | C) } or x in bool the carrier of M )
assume x in { (Int U) where U is Subset of M : U in rng (W | C) } ; :: thesis: x in bool the carrier of M
then ex U being Subset of M st
( x = Int U & U in rng (W | C) ) ;
hence x in bool the carrier of M ; :: thesis: verum
end;
then reconsider IntW = { (Int U) where U is Subset of M : U in rng (W | C) } as Subset-Family of M ;
reconsider R = IntW \/ {(C `)} as Subset-Family of M ;
for A being Subset of M st A in R holds
A is open
proof
let A be Subset of M; :: thesis: ( A in R implies A is open )
assume A5: A in R ; :: thesis: A is open
per cases ( A = C ` or A in IntW ) by ;
suppose A in IntW ; :: thesis: A is open
then ex U being Subset of M st
( A = Int U & U in rng (W | C) ) ;
hence A is open ; :: thesis: verum
end;
end;
end;
then A6: R is open by TOPS_2:def 1;
A7: for A being Subset of M st A in rng W holds
( A is connected & not Int A is empty )
proof
let A be Subset of M; :: thesis: ( A in rng W implies ( A is connected & not Int A is empty ) )
assume A in rng W ; :: thesis: ( A is connected & not Int A is empty )
then consider p being object such that
A8: p in dom W and
A9: W . p = A by FUNCT_1:def 3;
consider n being Nat such that
A10: M | A, Tdisk ((0. ()),1) are_homeomorphic by A8, A9, A4;
reconsider AA = A as non empty Subset of M by A8, A9, A4;
A11: Tdisk ((0. ()),1) is connected by CONNSP_1:def 3;
Tdisk ((0. ()),1),M | AA are_homeomorphic by A10;
then consider h being Function of (Tdisk ((0. ()),1)),(M | A) such that
A12: h is being_homeomorphism by T_0TOPSP:def 1;
reconsider p = p as Point of M by A8;
A13: S1[p,A] by A8, A9, A4;
A14: rng h = [#] (M | A) by ;
A15: h .: (dom h) = rng h by RELAT_1:113;
dom h = [#] (Tdisk ((0. ()),1)) by ;
then M | A is connected by ;
hence ( A is connected & not Int A is empty ) by ; :: thesis: verum
end;
A16: dom W = the carrier of M by FUNCT_2:def 1;
the carrier of M c= union R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of M or x in union R )
assume x in the carrier of M ; :: thesis: x in union R
then reconsider x = x as Point of M ;
per cases ( x in C or not x in C ) ;
end;
end;
then consider R1 being Subset-Family of M such that
A21: R1 c= R and
A22: R1 is Cover of M and
A23: R1 is finite by ;
reconsider R1 = R1 as finite Subset-Family of M by A23;
set R2 = R1 \ {(C `)};
union R1 = the carrier of M by ;
then A24: (union R1) \ (union {(C `)}) = the carrier of M \ (C `) by ZFMISC_1:25
.= (C `) ` by SUBSET_1:def 4
.= C ;
then C c= union (R1 \ {(C `)}) by TOPS_2:4;
then consider xp being set such that
p in xp and
A25: xp in R1 \ {(C `)} by ;
A26: C = Component_of C by ;
for x being set holds
( x in C iff ex Q being Subset of M st
( Q is open & Q c= C & x in Q ) )
proof
let x be set ; :: thesis: ( x in C iff ex Q being Subset of M st
( Q is open & Q c= C & x in Q ) )

hereby :: thesis: ( ex Q being Subset of M st
( Q is open & Q c= C & x in Q ) implies x in C )
assume A27: x in C ; :: thesis: ex I being Element of bool the carrier of M st
( I is open & I c= C & x in I )

then reconsider p = x as Point of M ;
take I = Int (W . p); :: thesis: ( I is open & I c= C & x in I )
A28: Int (W . p) c= W . p by TOPS_1:16;
W . p in rng W by ;
then A29: W . p is connected by A7;
A30: W . p is a_neighborhood of p by A4;
then p in Int (W . p) by CONNSP_2:def 1;
then W . p meets C by ;
then W . p c= C by ;
hence ( I is open & I c= C & x in I ) by ; :: thesis: verum
end;
thus ( ex Q being Subset of M st
( Q is open & Q c= C & x in Q ) implies x in C ) ; :: thesis: verum
end;
hence C is open by TOPS_1:25; :: thesis: ex n being Nat st M | C is non empty b1 -locally_euclidean TopSpace
A31: R1 \ {(C `)} c= R1 by XBOOLE_1:36;
A32: rng (W | C) c= rng W by RELAT_1:70;
union (R1 \ {(C `)}) c= C
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (R1 \ {(C `)}) or x in C )
assume x in union (R1 \ {(C `)}) ; :: thesis: x in C
then consider y being set such that
A33: x in y and
A34: y in R1 \ {(C `)} by TARSKI:def 4;
y in R1 by ;
then ( y in IntW or y = C ` ) by ;
then consider U being Subset of M such that
A35: y = Int U and
A36: U in rng (W | C) by ;
A37: U is connected by A32, A36, A7;
A38: Int U c= U by TOPS_1:16;
consider p being object such that
A39: p in dom (W | C) and
A40: (W | C) . p = U by ;
A41: W . p = U by ;
p in dom W by ;
then reconsider p = p as Point of M ;
U is a_neighborhood of p by ;
then p in Int U by CONNSP_2:def 1;
then W . p meets C by ;
then U c= C by ;
hence x in C by ; :: thesis: verum
end;
then A42: union (R1 \ {(C `)}) = C by ;
A43: for x being object st x in R1 \ {(C `)} holds
ex y being object st S2[x,y]
proof
let x be object ; :: thesis: ( x in R1 \ {(C `)} implies ex y being object st S2[x,y] )
assume A44: x in R1 \ {(C `)} ; :: thesis: ex y being object st S2[x,y]
then A45: x <> C ` by ZFMISC_1:56;
x in R1 by ;
then x in IntW by ;
then consider U being Subset of M such that
A46: x = Int U and
A47: U in rng (W | C) ;
consider y being object such that
A48: y in dom (W | C) and
A49: (W | C) . y = U by ;
take y ; :: thesis: S2[x,y]
thus y in C by A48; :: thesis: for A being Subset of M st A = W . y holds
Int A = x

let A be Subset of M; :: thesis: ( A = W . y implies Int A = x )
thus ( A = W . y implies Int A = x ) by ; :: thesis: verum
end;
consider cc being Function such that
A50: ( dom cc = R1 \ {(C `)} & ( for x being object st x in R1 \ {(C `)} holds
S2[x,cc . x] ) ) from S2[xp,cc . xp] by ;
then reconsider cp = cc . xp as Point of M ;
consider n being Nat such that
A51: M | (W . cp), Tdisk ((0. ()),1) are_homeomorphic by A4;
defpred S3[ Nat] means ( \$1 <= card (R1 \ {(C `)}) implies ex R3 being Subset-Family of M st
( card R3 = \$1 & R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) ) );
A52: Int (W . cp) = xp by ;
A53: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A54: S3[k] ; :: thesis: S3[k + 1]
assume A55: k + 1 <= card (R1 \ {(C `)}) ; :: thesis: ex R3 being Subset-Family of M st
( card R3 = k + 1 & R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

then consider R3 being Subset-Family of M such that
A56: card R3 = k and
A57: R3 c= R1 \ {(C `)} and
A58: union (W .: (cc .: R3)) is connected Subset of M and
A59: for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic by ;
k < card (R1 \ {(C `)}) by ;
then k in Segm (card (R1 \ {(C `)})) by NAT_1:44;
then (R1 \ {(C `)}) \ R3 <> {} by ;
then consider r23 being object such that
A60: r23 in (R1 \ {(C `)}) \ R3 by XBOOLE_0:def 1;
reconsider r23 = r23 as set by TARSKI:1;
A61: r23 in R1 \ {(C `)} by ;
then A62: r23 <> C ` by ZFMISC_1:56;
r23 in R1 by ;
then r23 in IntW by ;
then A63: ex B being Subset of M st
( Int B = r23 & B in rng (W | C) ) ;
A64: r23 c= union ((R1 \ {(C `)}) \ R3) by ;
per cases ( k > 0 or k = 0 ) ;
suppose k > 0 ; :: thesis: ex R3 being Subset-Family of M st
( card R3 = k + 1 & R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

then not R3 is empty by A56;
then consider r3 being set such that
A65: r3 in R3 ;
A66: r3 <> C ` by ;
r3 in R1 by ;
then r3 in IntW by ;
then A67: ex A being Subset of M st
( Int A = r3 & A in rng (W | C) ) ;
r3 c= union R3 by ;
then reconsider U3 = union R3 as non empty Subset of M by A32, A67, A7;
set A1 = the Subset of M;
reconsider U23 = union ((R1 \ {(C `)}) \ R3) as Subset of M ;
set D2 = Down (U3,C);
set D23 = Down (U23,C);
Down (U3,C) = U3 /\ C by CONNSP_3:def 5;
then A68: Down (U3,C) = U3 by ;
((R1 \ {(C `)}) \ R3) \/ R3 = (R1 \ {(C `)}) \/ R3 by XBOOLE_1:39
.= R1 \ {(C `)} by ;
then U3 \/ U23 = C by ;
then A69: U3 \/ U23 = [#] MC by PRE_TOPC:def 5;
R3 c= R1 by ;
then R3 is open by ;
then A70: Down (U3,C) is open by ;
A71: (R1 \ {(C `)}) \ R3 c= R1 \ {(C `)} by XBOOLE_1:36;
then (R1 \ {(C `)}) \ R3 c= R1 by A31;
then (R1 \ {(C `)}) \ R3 is open by ;
then A72: Down (U23,C) is open by ;
Down (U23,C) = U23 /\ C by CONNSP_3:def 5;
then A73: Down (U23,C) = U23 by ;
U23 <> {} MC by A64, A32, A63, A7;
then consider m being object such that
A74: m in U3 and
A75: m in U23 by ;
consider m1 being set such that
A76: m in m1 and
A77: m1 in R3 by ;
S2[m1,cc . m1] by ;
then reconsider c1 = cc . m1 as Point of M ;
consider m2 being set such that
A78: m in m2 and
A79: m2 in (R1 \ {(C `)}) \ R3 by ;
A80: m2 in R1 \ {(C `)} by ;
then S2[m2,cc . m2] by A50;
then reconsider c2 = cc . m2 as Point of M ;
set R4 = R3 \/ {(Int (W . c2))};
R3 is finite by A56;
then reconsider R4 = R3 \/ {(Int (W . c2))} as finite Subset-Family of M ;
take R4 ; :: thesis: ( card R4 = k + 1 & R4 c= R1 \ {(C `)} & union (W .: (cc .: R4)) is connected Subset of M & ( for A, B being Subset of M st A in R4 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

A81: Int (W . c2) = m2 by ;
then not Int (W . c2) in R3 by ;
hence card R4 = k + 1 by ; :: thesis: ( R4 c= R1 \ {(C `)} & union (W .: (cc .: R4)) is connected Subset of M & ( for A, B being Subset of M st A in R4 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

A82: m2 in R1 \ {(C `)} by ;
then {m2} c= R1 \ {(C `)} by ZFMISC_1:31;
hence A83: R4 c= R1 \ {(C `)} by ; :: thesis: ( union (W .: (cc .: R4)) is connected Subset of M & ( for A, B being Subset of M st A in R4 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

A84: W . c2 in rng W by ;
A85: Int (W . c1) = m1 by ;
thus union (W .: (cc .: R4)) is connected Subset of M :: thesis: for A, B being Subset of M st A in R4 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic
proof
reconsider UWR3 = union (W .: (cc .: R3)) as connected Subset of M by A58;
A86: Int (W . c2) c= W . c2 by TOPS_1:16;
c1 in cc .: R3 by ;
then A87: W . c1 in W .: (cc .: R3) by ;
Int (W . c1) c= W . c1 by TOPS_1:16;
then A88: m in UWR3 by ;
UWR3 c= Cl UWR3 by PRE_TOPC:18;
then Cl UWR3 meets W . c2 by ;
then A89: not UWR3,W . c2 are_separated by CONNSP_1:def 1;
cc .: R4 = (cc .: R3) \/ (cc .: {m2}) by
.= (cc .: R3) \/ (Im (cc,m2)) by RELAT_1:def 16
.= (cc .: R3) \/ {(cc . m2)} by ;
then W .: (cc .: R4) = (W .: (cc .: R3)) \/ (W .: {c2}) by RELAT_1:120
.= (W .: (cc .: R3)) \/ (Im (W,c2)) by RELAT_1:def 16
.= (W .: (cc .: R3)) \/ {(W . c2)} by ;
then A90: union (W .: (cc .: R4)) = UWR3 \/ (union {(W . c2)}) by ZFMISC_1:78
.= UWR3 \/ (W . c2) by ZFMISC_1:25 ;
W . c2 is connected by ;
hence union (W .: (cc .: R4)) is connected Subset of M by ; :: thesis: verum
end;
let a, b be Subset of M; :: thesis: ( a in R4 & b = W . (cc . a) implies M | b, Tdisk ((0. ()),1) are_homeomorphic )
assume that
A91: a in R4 and
A92: b = W . (cc . a) ; :: thesis: M | b, Tdisk ((0. ()),1) are_homeomorphic
per cases ( a in R3 or a = Int (W . c2) ) by ;
suppose a in R3 ; :: thesis: M | b, Tdisk ((0. ()),1) are_homeomorphic
hence M | b, Tdisk ((0. ()),1) are_homeomorphic by ; :: thesis: verum
end;
suppose a = Int (W . c2) ; :: thesis: M | b, Tdisk ((0. ()),1) are_homeomorphic
then Int b = Int (W . c2) by ;
then A93: m in Int b by ;
S2[a,cc . a] by ;
then reconsider ca = cc . a as Point of M ;
A94: M | (W . c1), Tdisk ((0. ()),1) are_homeomorphic by ;
S1[ca,W . ca] by A4;
then consider mm being Nat such that
A95: M | b, Tdisk ((0. (TOP-REAL mm)),1) are_homeomorphic by A92;
Int (W . c1) = m1 by ;
then n = mm by ;
hence M | b, Tdisk ((0. ()),1) are_homeomorphic by A95; :: thesis: verum
end;
end;
end;
suppose A96: k = 0 ; :: thesis: ex R3 being Subset-Family of M st
( card R3 = k + 1 & R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

reconsider R3 = {(Int (W . cp))} as Subset-Family of M ;
take R3 ; :: thesis: ( card R3 = k + 1 & R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

thus card R3 = k + 1 by ; :: thesis: ( R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

thus A97: R3 c= R1 \ {(C `)} by ; :: thesis: ( union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

cc .: R3 = Im (cc,xp) by
.= {cp} by ;
then W .: (cc .: R3) = Im (W,cp) by RELAT_1:def 16
.= {(W . cp)} by ;
then A98: union (W .: (cc .: R3)) = W . cp by ZFMISC_1:25;
W . cp in rng W by ;
hence union (W .: (cc .: R3)) is connected Subset of M by ; :: thesis: for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic

let a, b be Subset of M; :: thesis: ( a in R3 & b = W . (cc . a) implies M | b, Tdisk ((0. ()),1) are_homeomorphic )
assume that
A99: a in R3 and
A100: b = W . (cc . a) ; :: thesis: M | b, Tdisk ((0. ()),1) are_homeomorphic
S2[a,cc . a] by ;
then reconsider ca = cc . a as Point of M ;
Int (W . cp) = xp by ;
hence M | b, Tdisk ((0. ()),1) are_homeomorphic by ; :: thesis: verum
end;
end;
end;
take n ; :: thesis: M | C is non empty n -locally_euclidean TopSpace
A101: S3[ 0 ]
proof
set R3 = the empty Subset of (bool the carrier of M);
assume 0 <= card (R1 \ {(C `)}) ; :: thesis: ex R3 being Subset-Family of M st
( card R3 = 0 & R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

take the empty Subset of (bool the carrier of M) ; :: thesis: ( card the empty Subset of (bool the carrier of M) = 0 & the empty Subset of (bool the carrier of M) c= R1 \ {(C `)} & union (W .: (cc .: the empty Subset of (bool the carrier of M))) is connected Subset of M & ( for A, B being Subset of M st A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

thus ( card the empty Subset of (bool the carrier of M) = 0 & the empty Subset of (bool the carrier of M) c= R1 \ {(C `)} ) ; :: thesis: ( union (W .: (cc .: the empty Subset of (bool the carrier of M))) is connected Subset of M & ( for A, B being Subset of M st A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ) )

reconsider UR3 = union (W .: (cc .: the empty Subset of (bool the carrier of M))) as empty Subset of M by ZFMISC_1:2;
UR3 is connected ;
hence union (W .: (cc .: the empty Subset of (bool the carrier of M))) is connected Subset of M ; :: thesis: for A, B being Subset of M st A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic

let A, B be Subset of M; :: thesis: ( A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) implies M | B, Tdisk ((0. ()),1) are_homeomorphic )
thus ( A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) implies M | B, Tdisk ((0. ()),1) are_homeomorphic ) ; :: thesis: verum
end;
for k being Nat holds S3[k] from then S3[ card (R1 \ {(C `)})] ;
then consider R3 being Subset-Family of M such that
A102: card R3 = card (R1 \ {(C `)}) and
A103: R3 c= R1 \ {(C `)} and
A104: for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. ()),1) are_homeomorphic ;
A105: R1 \ {(C `)} = R3 by ;
for p being Point of MC ex U being a_neighborhood of p st MC | U, Tdisk ((0. ()),1) are_homeomorphic
proof
let q be Point of MC; :: thesis: ex U being a_neighborhood of q st MC | U, Tdisk ((0. ()),1) are_homeomorphic
A106: [#] MC = C by PRE_TOPC:def 5;
then consider y being set such that
A107: q in y and
A108: y in R1 \ {(C `)} by ;
S2[y,cc . y] by ;
then reconsider c = cc . y as Point of M ;
reconsider Wc = W . c as Subset of M ;
A109: Int Wc c= Wc by TOPS_1:16;
set D = Down (Wc,C);
set DI = Down ((Int Wc),C);
Wc in rng W by ;
then A110: Wc is connected by A7;
A111: Int Wc = y by ;
then Wc meets C by ;
then A112: Wc c= C by ;
then (W . c) /\ C = W . c by XBOOLE_1:28;
then A113: Down (Wc,C) = W . c by CONNSP_3:def 5;
(Int Wc) /\ C = Int Wc by ;
then Down ((Int Wc),C) = Int Wc by CONNSP_3:def 5;
then q in Int (Down (Wc,C)) by ;
then A114: Down (Wc,C) is a_neighborhood of q by CONNSP_2:def 1;
M | (W . c) = (M | C) | (Down (Wc,C)) by ;
hence ex U being a_neighborhood of q st MC | U, Tdisk ((0. ()),1) are_homeomorphic by ; :: thesis: verum
end;
hence M | C is non empty n -locally_euclidean TopSpace by Def3; :: thesis: verum