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 b_{2} -locally_euclidean TopSpace )

defpred S_{1}[ Point of M, Subset of M] means ( $2 is a_neighborhood of $1 & ex n being Nat st M | $2, Tdisk ((0. (TOP-REAL n)),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 b_{1} -locally_euclidean TopSpace ) )

assume A1: C is a_component ; :: thesis: ( C is open & ex n being Nat st M | C is non empty b_{1} -locally_euclidean TopSpace )

consider p being object such that

A2: p in C by A1, XBOOLE_0:def 1;

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 S_{1}[x,y]

A4: for x being Point of M holds S_{1}[x,W . x]
from FUNCT_2:sch 3(A3);

reconsider MC = M | C as non empty connected TopSpace by A1, CONNSP_1:def 3;

defpred S_{2}[ 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

reconsider R = IntW \/ {(C `)} as Subset-Family of M ;

for A being Subset of M st A in R holds

A is open

A7: for A being Subset of M st A in rng W holds

( A is connected & not Int A is empty )

the carrier of M c= union R

A21: R1 c= R and

A22: R1 is Cover of M and

A23: R1 is finite by SETFAM_1:def 11, A6, COMPTS_1:def 1;

reconsider R1 = R1 as finite Subset-Family of M by A23;

set R2 = R1 \ {(C `)};

union R1 = the carrier of M by A22, SETFAM_1:45;

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 A2, TARSKI:def 4;

A26: C = Component_of C by A1, CONNSP_3:7;

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 ) )_{1} -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

A43: for x being object st x in R1 \ {(C `)} holds

ex y being object st S_{2}[x,y]

A50: ( dom cc = R1 \ {(C `)} & ( for x being object st x in R1 \ {(C `)} holds

S_{2}[x,cc . x] ) )
from CLASSES1:sch 1(A43);

S_{2}[xp,cc . xp]
by A25, A50;

then reconsider cp = cc . xp as Point of M ;

consider n being Nat such that

A51: M | (W . cp), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A4;

defpred S_{3}[ 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. (TOP-REAL n)),1) are_homeomorphic ) ) );

A52: Int (W . cp) = xp by A25, A50;

A53: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]

A101: S_{3}[ 0 ]
_{3}[k]
from NAT_1:sch 2(A101, A53);

then S_{3}[ 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. (TOP-REAL n)),1) are_homeomorphic ;

A105: R1 \ {(C `)} = R3 by A102, A103, CARD_2:102;

for p being Point of MC ex U being a_neighborhood of p st MC | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

( C is open & ex n being Nat st M | C is non empty b

defpred S

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 b

assume A1: C is a_component ; :: thesis: ( C is open & ex n being Nat st M | C is non empty b

consider p being object such that

A2: p in C by A1, XBOOLE_0:def 1;

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 S

proof

consider W being Function of M,(bool the carrier of M) such that
let x be Point of M; :: thesis: ex y being Element of bool the carrier of M st S_{1}[x,y]

ex U being a_neighborhood of x ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def2;

hence ex y being Element of bool the carrier of M st S_{1}[x,y]
; :: thesis: verum

end;ex U being a_neighborhood of x ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def2;

hence ex y being Element of bool the carrier of M st S

A4: for x being Point of M holds S

reconsider MC = M | C as non empty connected TopSpace by A1, CONNSP_1:def 3;

defpred S

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

then reconsider IntW = { (Int U) where U is Subset of M : U in rng (W | C) } as Subset-Family of M ;
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;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

reconsider R = IntW \/ {(C `)} as Subset-Family of M ;

for A being Subset of M st A in R holds

A is open

proof

then A6:
R is open
by TOPS_2:def 1;
let A be Subset of M; :: thesis: ( A in R implies A is open )

assume A5: A in R ; :: thesis: A is open

end;assume A5: A in R ; :: thesis: A is open

A7: for A being Subset of M st A in rng W holds

( A is connected & not Int A is empty )

proof

A16:
dom W = the carrier of M
by FUNCT_2:def 1;
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. (TOP-REAL n)),1) are_homeomorphic by A8, A9, A4;

reconsider AA = A as non empty Subset of M by A8, A9, A4;

A11: Tdisk ((0. (TOP-REAL n)),1) is connected by CONNSP_1:def 3;

Tdisk ((0. (TOP-REAL n)),1),M | AA are_homeomorphic by A10;

then consider h being Function of (Tdisk ((0. (TOP-REAL n)),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: S_{1}[p,A]
by A8, A9, A4;

A14: rng h = [#] (M | A) by A12, TOPS_2:def 5;

A15: h .: (dom h) = rng h by RELAT_1:113;

dom h = [#] (Tdisk ((0. (TOP-REAL n)),1)) by A12, TOPS_2:def 5;

then M | A is connected by A15, A14, A12, A11, CONNSP_1:14;

hence ( A is connected & not Int A is empty ) by CONNSP_1:def 3, A13, CONNSP_2:def 1; :: thesis: verum

end;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. (TOP-REAL n)),1) are_homeomorphic by A8, A9, A4;

reconsider AA = A as non empty Subset of M by A8, A9, A4;

A11: Tdisk ((0. (TOP-REAL n)),1) is connected by CONNSP_1:def 3;

Tdisk ((0. (TOP-REAL n)),1),M | AA are_homeomorphic by A10;

then consider h being Function of (Tdisk ((0. (TOP-REAL n)),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: S

A14: rng h = [#] (M | A) by A12, TOPS_2:def 5;

A15: h .: (dom h) = rng h by RELAT_1:113;

dom h = [#] (Tdisk ((0. (TOP-REAL n)),1)) by A12, TOPS_2:def 5;

then M | A is connected by A15, A14, A12, A11, CONNSP_1:14;

hence ( A is connected & not Int A is empty ) by CONNSP_1:def 3, A13, CONNSP_2:def 1; :: thesis: verum

the carrier of M c= union R

proof

then consider R1 being Subset-Family of M such that
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 ;

end;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;

suppose
x in C
; :: thesis: x in union R

then A17:
x in dom (W | C)
by RELAT_1:57, A16;

then A18: (W | C) . x = W . x by FUNCT_1:47;

(W | C) . x in rng (W | C) by A17, FUNCT_1:def 3;

then Int (W . x) in IntW by A18;

then A19: Int (W . x) in R by XBOOLE_0:def 3;

W . x is a_neighborhood of x by A4;

then x in Int (W . x) by CONNSP_2:def 1;

hence x in union R by A19, TARSKI:def 4; :: thesis: verum

end;then A18: (W | C) . x = W . x by FUNCT_1:47;

(W | C) . x in rng (W | C) by A17, FUNCT_1:def 3;

then Int (W . x) in IntW by A18;

then A19: Int (W . x) in R by XBOOLE_0:def 3;

W . x is a_neighborhood of x by A4;

then x in Int (W . x) by CONNSP_2:def 1;

hence x in union R by A19, TARSKI:def 4; :: thesis: verum

suppose
not x in C
; :: thesis: x in union R

then
x in ([#] M) \ C
by XBOOLE_0:def 5;

then A20: x in C ` by SUBSET_1:def 4;

C ` in R by ZFMISC_1:136;

hence x in union R by A20, TARSKI:def 4; :: thesis: verum

end;then A20: x in C ` by SUBSET_1:def 4;

C ` in R by ZFMISC_1:136;

hence x in union R by A20, TARSKI:def 4; :: thesis: verum

A21: R1 c= R and

A22: R1 is Cover of M and

A23: R1 is finite by SETFAM_1:def 11, A6, COMPTS_1:def 1;

reconsider R1 = R1 as finite Subset-Family of M by A23;

set R2 = R1 \ {(C `)};

union R1 = the carrier of M by A22, SETFAM_1:45;

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 A2, TARSKI:def 4;

A26: C = Component_of C by A1, CONNSP_3:7;

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

hence
C is open
by TOPS_1:25; :: thesis: ex n being Nat st M | C is non empty b
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 ) )

( Q is open & Q c= C & x in Q ) implies x in C ) ; :: thesis: verum

end;( 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 )

thus
( 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 A16, FUNCT_1:def 3;

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 A28, A27, XBOOLE_0:3;

then W . p c= C by A1, A29, CONNSP_3:16, A26;

hence ( I is open & I c= C & x in I ) by A30, CONNSP_2:def 1, A28; :: thesis: verum

end;( 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 A16, FUNCT_1:def 3;

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 A28, A27, XBOOLE_0:3;

then W . p c= C by A1, A29, CONNSP_3:16, A26;

hence ( I is open & I c= C & x in I ) by A30, CONNSP_2:def 1, A28; :: thesis: verum

( Q is open & Q c= C & x in Q ) implies x in C ) ; :: thesis: verum

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

then A42:
union (R1 \ {(C `)}) = C
by A24, TOPS_2:4;
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 A34, ZFMISC_1:56;

then ( y in IntW or y = C ` ) by A21, ZFMISC_1:136;

then consider U being Subset of M such that

A35: y = Int U and

A36: U in rng (W | C) by A34, ZFMISC_1:56;

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 A36, FUNCT_1:def 3;

A41: W . p = U by A39, A40, FUNCT_1:47;

p in dom W by A39, RELAT_1:57;

then reconsider p = p as Point of M ;

U is a_neighborhood of p by A4, A41;

then p in Int U by CONNSP_2:def 1;

then W . p meets C by A38, A39, A41, XBOOLE_0:3;

then U c= C by A41, A1, A37, CONNSP_3:16, A26;

hence x in C by A38, A33, A35; :: thesis: verum

end;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 A34, ZFMISC_1:56;

then ( y in IntW or y = C ` ) by A21, ZFMISC_1:136;

then consider U being Subset of M such that

A35: y = Int U and

A36: U in rng (W | C) by A34, ZFMISC_1:56;

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 A36, FUNCT_1:def 3;

A41: W . p = U by A39, A40, FUNCT_1:47;

p in dom W by A39, RELAT_1:57;

then reconsider p = p as Point of M ;

U is a_neighborhood of p by A4, A41;

then p in Int U by CONNSP_2:def 1;

then W . p meets C by A38, A39, A41, XBOOLE_0:3;

then U c= C by A41, A1, A37, CONNSP_3:16, A26;

hence x in C by A38, A33, A35; :: thesis: verum

A43: for x being object st x in R1 \ {(C `)} holds

ex y being object st S

proof

consider cc being Function such that
let x be object ; :: thesis: ( x in R1 \ {(C `)} implies ex y being object st S_{2}[x,y] )

assume A44: x in R1 \ {(C `)} ; :: thesis: ex y being object st S_{2}[x,y]

then A45: x <> C ` by ZFMISC_1:56;

x in R1 by A44, ZFMISC_1:56;

then x in IntW by A21, A45, ZFMISC_1:136;

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 A47, FUNCT_1:def 3;

take y ; :: thesis: S_{2}[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 A48, FUNCT_1:47, A46, A49; :: thesis: verum

end;assume A44: x in R1 \ {(C `)} ; :: thesis: ex y being object st S

then A45: x <> C ` by ZFMISC_1:56;

x in R1 by A44, ZFMISC_1:56;

then x in IntW by A21, A45, ZFMISC_1:136;

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 A47, FUNCT_1:def 3;

take y ; :: thesis: S

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 A48, FUNCT_1:47, A46, A49; :: thesis: verum

A50: ( dom cc = R1 \ {(C `)} & ( for x being object st x in R1 \ {(C `)} holds

S

S

then reconsider cp = cc . xp as Point of M ;

consider n being Nat such that

A51: M | (W . cp), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A4;

defpred S

( 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. (TOP-REAL n)),1) are_homeomorphic ) ) );

A52: Int (W . cp) = xp by A25, A50;

A53: for k being Nat st S

S

proof

take
n
; :: thesis: M | C is non empty n -locally_euclidean TopSpace
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

assume A54: S_{3}[k]
; :: thesis: S_{3}[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. (TOP-REAL n)),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. (TOP-REAL n)),1) are_homeomorphic by NAT_1:13, A54;

k < card (R1 \ {(C `)}) by A55, NAT_1:13;

then k in Segm (card (R1 \ {(C `)})) by NAT_1:44;

then (R1 \ {(C `)}) \ R3 <> {} by A56, CARD_1:68;

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 A60, XBOOLE_0:def 5;

then A62: r23 <> C ` by ZFMISC_1:56;

r23 in R1 by A61, ZFMISC_1:56;

then r23 in IntW by A21, A62, ZFMISC_1:136;

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 A60, ZFMISC_1:74;

end;assume A54: S

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. (TOP-REAL n)),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. (TOP-REAL n)),1) are_homeomorphic by NAT_1:13, A54;

k < card (R1 \ {(C `)}) by A55, NAT_1:13;

then k in Segm (card (R1 \ {(C `)})) by NAT_1:44;

then (R1 \ {(C `)}) \ R3 <> {} by A56, CARD_1:68;

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 A60, XBOOLE_0:def 5;

then A62: r23 <> C ` by ZFMISC_1:56;

r23 in R1 by A61, ZFMISC_1:56;

then r23 in IntW by A21, A62, ZFMISC_1:136;

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 A60, ZFMISC_1:74;

per cases
( k > 0 or k = 0 )
;

end;

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. (TOP-REAL n)),1) are_homeomorphic ) )

( 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. (TOP-REAL n)),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 A57, A65, ZFMISC_1:56;

r3 in R1 by A57, A65, ZFMISC_1:56;

then r3 in IntW by A21, A66, ZFMISC_1:136;

then A67: ex A being Subset of M st

( Int A = r3 & A in rng (W | C) ) ;

r3 c= union R3 by A65, ZFMISC_1:74;

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 XBOOLE_1:28, A42, A57, ZFMISC_1:77;

((R1 \ {(C `)}) \ R3) \/ R3 = (R1 \ {(C `)}) \/ R3 by XBOOLE_1:39

.= R1 \ {(C `)} by A57, XBOOLE_1:12 ;

then U3 \/ U23 = C by A42, ZFMISC_1:78;

then A69: U3 \/ U23 = [#] MC by PRE_TOPC:def 5;

R3 c= R1 by A31, A57;

then R3 is open by A21, XBOOLE_1:1, A6, TOPS_2:11;

then A70: Down (U3,C) is open by TOPS_2:19, CONNSP_3:28;

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 A21, XBOOLE_1:1, A6, TOPS_2:11;

then A72: Down (U23,C) is open by TOPS_2:19, CONNSP_3:28;

Down (U23,C) = U23 /\ C by CONNSP_3:def 5;

then A73: Down (U23,C) = U23 by XBOOLE_1:28, A71, A42, ZFMISC_1:77;

U23 <> {} MC by A64, A32, A63, A7;

then consider m being object such that

A74: m in U3 and

A75: m in U23 by A70, A72, A68, A73, A69, CONNSP_1:11, XBOOLE_0:3;

consider m1 being set such that

A76: m in m1 and

A77: m1 in R3 by A74, TARSKI:def 4;

S_{2}[m1,cc . m1]
by A57, A77, A50;

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 A75, TARSKI:def 4;

A80: m2 in R1 \ {(C `)} by A79, XBOOLE_0:def 5;

then S_{2}[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. (TOP-REAL n)),1) are_homeomorphic ) )

A81: Int (W . c2) = m2 by A80, A50;

then not Int (W . c2) in R3 by A79, XBOOLE_0:def 5;

hence card R4 = k + 1 by A56, A57, CARD_2:41; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

A82: m2 in R1 \ {(C `)} by A79, XBOOLE_0:def 5;

then {m2} c= R1 \ {(C `)} by ZFMISC_1:31;

hence A83: R4 c= R1 \ {(C `)} by A81, A57, XBOOLE_1:8; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

A84: W . c2 in rng W by A16, FUNCT_1:def 3;

A85: Int (W . c1) = m1 by A57, A77, A50;

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. (TOP-REAL n)),1) are_homeomorphic

assume that

A91: a in R4 and

A92: b = W . (cc . a) ; :: thesis: M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

end;then consider r3 being set such that

A65: r3 in R3 ;

A66: r3 <> C ` by A57, A65, ZFMISC_1:56;

r3 in R1 by A57, A65, ZFMISC_1:56;

then r3 in IntW by A21, A66, ZFMISC_1:136;

then A67: ex A being Subset of M st

( Int A = r3 & A in rng (W | C) ) ;

r3 c= union R3 by A65, ZFMISC_1:74;

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 XBOOLE_1:28, A42, A57, ZFMISC_1:77;

((R1 \ {(C `)}) \ R3) \/ R3 = (R1 \ {(C `)}) \/ R3 by XBOOLE_1:39

.= R1 \ {(C `)} by A57, XBOOLE_1:12 ;

then U3 \/ U23 = C by A42, ZFMISC_1:78;

then A69: U3 \/ U23 = [#] MC by PRE_TOPC:def 5;

R3 c= R1 by A31, A57;

then R3 is open by A21, XBOOLE_1:1, A6, TOPS_2:11;

then A70: Down (U3,C) is open by TOPS_2:19, CONNSP_3:28;

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 A21, XBOOLE_1:1, A6, TOPS_2:11;

then A72: Down (U23,C) is open by TOPS_2:19, CONNSP_3:28;

Down (U23,C) = U23 /\ C by CONNSP_3:def 5;

then A73: Down (U23,C) = U23 by XBOOLE_1:28, A71, A42, ZFMISC_1:77;

U23 <> {} MC by A64, A32, A63, A7;

then consider m being object such that

A74: m in U3 and

A75: m in U23 by A70, A72, A68, A73, A69, CONNSP_1:11, XBOOLE_0:3;

consider m1 being set such that

A76: m in m1 and

A77: m1 in R3 by A74, TARSKI:def 4;

S

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 A75, TARSKI:def 4;

A80: m2 in R1 \ {(C `)} by A79, XBOOLE_0:def 5;

then S

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. (TOP-REAL n)),1) are_homeomorphic ) )

A81: Int (W . c2) = m2 by A80, A50;

then not Int (W . c2) in R3 by A79, XBOOLE_0:def 5;

hence card R4 = k + 1 by A56, A57, CARD_2:41; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

A82: m2 in R1 \ {(C `)} by A79, XBOOLE_0:def 5;

then {m2} c= R1 \ {(C `)} by ZFMISC_1:31;

hence A83: R4 c= R1 \ {(C `)} by A81, A57, XBOOLE_1:8; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

A84: W . c2 in rng W by A16, FUNCT_1:def 3;

A85: Int (W . c1) = m1 by A57, A77, A50;

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. (TOP-REAL n)),1) are_homeomorphic

proof

let a, b be Subset of M; :: thesis: ( a in R4 & b = W . (cc . a) implies M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic )
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 A77, A57, A50, FUNCT_1:def 6;

then A87: W . c1 in W .: (cc .: R3) by A16, FUNCT_1:def 6;

Int (W . c1) c= W . c1 by TOPS_1:16;

then A88: m in UWR3 by A87, A85, A76, TARSKI:def 4;

UWR3 c= Cl UWR3 by PRE_TOPC:18;

then Cl UWR3 meets W . c2 by A86, A81, A78, A88, XBOOLE_0:3;

then A89: not UWR3,W . c2 are_separated by CONNSP_1:def 1;

cc .: R4 = (cc .: R3) \/ (cc .: {m2}) by A81, RELAT_1:120

.= (cc .: R3) \/ (Im (cc,m2)) by RELAT_1:def 16

.= (cc .: R3) \/ {(cc . m2)} by FUNCT_1:59, A82, A50 ;

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 A16, FUNCT_1:59 ;

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 A84, A7;

hence union (W .: (cc .: R4)) is connected Subset of M by A89, CONNSP_1:17, A90; :: thesis: verum

end;A86: Int (W . c2) c= W . c2 by TOPS_1:16;

c1 in cc .: R3 by A77, A57, A50, FUNCT_1:def 6;

then A87: W . c1 in W .: (cc .: R3) by A16, FUNCT_1:def 6;

Int (W . c1) c= W . c1 by TOPS_1:16;

then A88: m in UWR3 by A87, A85, A76, TARSKI:def 4;

UWR3 c= Cl UWR3 by PRE_TOPC:18;

then Cl UWR3 meets W . c2 by A86, A81, A78, A88, XBOOLE_0:3;

then A89: not UWR3,W . c2 are_separated by CONNSP_1:def 1;

cc .: R4 = (cc .: R3) \/ (cc .: {m2}) by A81, RELAT_1:120

.= (cc .: R3) \/ (Im (cc,m2)) by RELAT_1:def 16

.= (cc .: R3) \/ {(cc . m2)} by FUNCT_1:59, A82, A50 ;

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 A16, FUNCT_1:59 ;

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 A84, A7;

hence union (W .: (cc .: R4)) is connected Subset of M by A89, CONNSP_1:17, A90; :: thesis: verum

assume that

A91: a in R4 and

A92: b = W . (cc . a) ; :: thesis: M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

per cases
( a in R3 or a = Int (W . c2) )
by A91, ZFMISC_1:136;

end;

suppose
a = Int (W . c2)
; :: thesis: M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

then
Int b = Int (W . c2)
by A80, A50, A92;

then A93: m in Int b by A80, A50, A78;

S_{2}[a,cc . a]
by A91, A83, A50;

then reconsider ca = cc . a as Point of M ;

A94: M | (W . c1), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A77, A59;

S_{1}[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 A57, A77, A50;

then n = mm by A94, A76, A93, XBOOLE_0:3, A95, BROUWER3:14;

hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A95; :: thesis: verum

end;then A93: m in Int b by A80, A50, A78;

S

then reconsider ca = cc . a as Point of M ;

A94: M | (W . c1), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A77, A59;

S

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 A57, A77, A50;

then n = mm by A94, A76, A93, XBOOLE_0:3, A95, BROUWER3:14;

hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A95; :: thesis: verum

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. (TOP-REAL n)),1) are_homeomorphic ) )

( 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. (TOP-REAL n)),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. (TOP-REAL n)),1) are_homeomorphic ) )

thus card R3 = k + 1 by A96, CARD_1:30; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

thus A97: R3 c= R1 \ {(C `)} by A52, A25, ZFMISC_1:31; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

cc .: R3 = Im (cc,xp) by A52, RELAT_1:def 16

.= {cp} by FUNCT_1:59, A25, A50 ;

then W .: (cc .: R3) = Im (W,cp) by RELAT_1:def 16

.= {(W . cp)} by A16, FUNCT_1:59 ;

then A98: union (W .: (cc .: R3)) = W . cp by ZFMISC_1:25;

W . cp in rng W by A16, FUNCT_1:def 3;

hence union (W .: (cc .: R3)) is connected Subset of M by A98, A7; :: thesis: for A, B being Subset of M st A in R3 & B = W . (cc . A) holds

M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

let a, b be Subset of M; :: thesis: ( a in R3 & b = W . (cc . a) implies M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic )

assume that

A99: a in R3 and

A100: b = W . (cc . a) ; :: thesis: M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

S_{2}[a,cc . a]
by A99, A97, A50;

then reconsider ca = cc . a as Point of M ;

Int (W . cp) = xp by A25, A50;

hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A51, TARSKI:def 1, A99, A100; :: thesis: verum

end;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. (TOP-REAL n)),1) are_homeomorphic ) )

thus card R3 = k + 1 by A96, CARD_1:30; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

thus A97: R3 c= R1 \ {(C `)} by A52, A25, ZFMISC_1:31; :: 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. (TOP-REAL n)),1) are_homeomorphic ) )

cc .: R3 = Im (cc,xp) by A52, RELAT_1:def 16

.= {cp} by FUNCT_1:59, A25, A50 ;

then W .: (cc .: R3) = Im (W,cp) by RELAT_1:def 16

.= {(W . cp)} by A16, FUNCT_1:59 ;

then A98: union (W .: (cc .: R3)) = W . cp by ZFMISC_1:25;

W . cp in rng W by A16, FUNCT_1:def 3;

hence union (W .: (cc .: R3)) is connected Subset of M by A98, A7; :: thesis: for A, B being Subset of M st A in R3 & B = W . (cc . A) holds

M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

let a, b be Subset of M; :: thesis: ( a in R3 & b = W . (cc . a) implies M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic )

assume that

A99: a in R3 and

A100: b = W . (cc . a) ; :: thesis: M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

S

then reconsider ca = cc . a as Point of M ;

Int (W . cp) = xp by A25, A50;

hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A51, TARSKI:def 1, A99, A100; :: thesis: verum

A101: S

proof

for k being Nat holds S
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. (TOP-REAL n)),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. (TOP-REAL n)),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. (TOP-REAL n)),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. (TOP-REAL n)),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. (TOP-REAL n)),1) are_homeomorphic )

thus ( A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) implies M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ) ; :: thesis: verum

end;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. (TOP-REAL n)),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. (TOP-REAL n)),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. (TOP-REAL n)),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. (TOP-REAL n)),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. (TOP-REAL n)),1) are_homeomorphic )

thus ( A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) implies M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ) ; :: thesis: verum

then S

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. (TOP-REAL n)),1) are_homeomorphic ;

A105: R1 \ {(C `)} = R3 by A102, A103, CARD_2:102;

for p being Point of MC ex U being a_neighborhood of p st MC | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

proof

hence
M | C is non empty n -locally_euclidean TopSpace
by Def3; :: thesis: verum
let q be Point of MC; :: thesis: ex U being a_neighborhood of q st MC | U, Tdisk ((0. (TOP-REAL n)),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 A42, TARSKI:def 4;

S_{2}[y,cc . y]
by A50, A108;

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 A16, FUNCT_1:def 3;

then A110: Wc is connected by A7;

A111: Int Wc = y by A50, A108;

then Wc meets C by A109, A107, A106, XBOOLE_0:3;

then A112: Wc c= C by A110, A1, CONNSP_3:16, A26;

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 A112, A109, XBOOLE_1:1, XBOOLE_1:28;

then Down ((Int Wc),C) = Int Wc by CONNSP_3:def 5;

then q in Int (Down (Wc,C)) by CONNSP_3:28, A107, A111, A113, A109, TOPS_1:22;

then A114: Down (Wc,C) is a_neighborhood of q by CONNSP_2:def 1;

M | (W . c) = (M | C) | (Down (Wc,C)) by A113, A106, PRE_TOPC:7;

hence ex U being a_neighborhood of q st MC | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A114, A104, A105, A108; :: thesis: verum

end;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 A42, TARSKI:def 4;

S

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 A16, FUNCT_1:def 3;

then A110: Wc is connected by A7;

A111: Int Wc = y by A50, A108;

then Wc meets C by A109, A107, A106, XBOOLE_0:3;

then A112: Wc c= C by A110, A1, CONNSP_3:16, A26;

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 A112, A109, XBOOLE_1:1, XBOOLE_1:28;

then Down ((Int Wc),C) = Int Wc by CONNSP_3:def 5;

then q in Int (Down (Wc,C)) by CONNSP_3:28, A107, A111, A113, A109, TOPS_1:22;

then A114: Down (Wc,C) is a_neighborhood of q by CONNSP_2:def 1;

M | (W . c) = (M | C) | (Down (Wc,C)) by A113, A106, PRE_TOPC:7;

hence ex U being a_neighborhood of q st MC | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A114, A104, A105, A108; :: thesis: verum