set MI = M | (Int M);

A1: [#] (M | (Int M)) = Int M by PRE_TOPC:def 5;

for p being Point of (M | (Int M)) ex U being a_neighborhood of p st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic_{1} being non empty TopSpace st b_{1} = M | (Int M) holds

b_{1} is n -locally_euclidean
by Th13; :: thesis: verum

A1: [#] (M | (Int M)) = Int M by PRE_TOPC:def 5;

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

proof

hence
for b
let p be Point of (M | (Int M)); :: thesis: ex U being a_neighborhood of p st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

p in Int M by A1;

then reconsider q = p as Point of M ;

consider U being a_neighborhood of q such that

A2: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1, Def7;

set MU = M | U;

set TR = TOP-REAL n;

consider h being Function of (M | U),(Tball ((0. (TOP-REAL n)),1)) such that

A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

A4: Int U c= U by TOPS_1:16;

A5: (Int M) /\ (Int U) in the topology of M by PRE_TOPC:def 2;

A6: Int U c= U by TOPS_1:16;

A7: [#] (M | U) = U by PRE_TOPC:def 5;

(Int U) /\ (Int M) c= Int U by XBOOLE_1:17;

then reconsider UIM = (Int M) /\ (Int U) as Subset of (M | U) by A6, A7, XBOOLE_1:1;

A8: h " (h .: UIM) c= UIM by A3, FUNCT_1:82;

A9: dom h = [#] (M | U) by A3, TOPS_2:def 5;

A11: [#] (Tball ((0. (TOP-REAL n)),1)) = Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider hum = h .: UIM as Subset of (TOP-REAL n) by XBOOLE_1:1;

UIM /\ ([#] (M | U)) = UIM by XBOOLE_1:28;

then UIM in the topology of (M | U) by A5, PRE_TOPC:def 4;

then UIM is open by PRE_TOPC:def 2;

then h .: UIM is open by A3, TOPGRP_1:25;

then hum is open by TSEP_1:9, A11;

then A12: Int hum = hum by TOPS_1:23;

A13: q in Int U by CONNSP_2:def 1;

then A14: q in UIM by A1, XBOOLE_0:def 4;

then h . q in hum by A9, FUNCT_1:def 6;

then reconsider hq = h . q as Point of (TOP-REAL n) ;

reconsider HQ = hq as Point of (Euclid n) by EUCLID:67;

h . q in h .: UIM by A14, A9, FUNCT_1:def 6;

then consider s being Real such that

A15: s > 0 and

A16: Ball (HQ,s) c= hum by A12, GOBOARD6:5;

A17: Ball (HQ,s) = Ball (hq,s) by TOPREAL9:13;

then reconsider BB = Ball (hq,s) as Subset of (Tball ((0. (TOP-REAL n)),1)) by A16, XBOOLE_1:1;

BB is open by TSEP_1:9;

then reconsider hBB = h " BB as open Subset of (M | U) by A3, TOPGRP_1:26;

hBB c= h " (h .: UIM) by A16, A17, RELAT_1:143;

then A18: hBB c= UIM by A8;

reconsider hBBM = hBB as Subset of M by A7, XBOOLE_1:1;

(Int U) /\ (Int M) c= Int M by XBOOLE_1:17;

then reconsider HBB = hBBM as Subset of (M | (Int M)) by A18, XBOOLE_1:1, A1;

hBBM is open by TSEP_1:9, A18;

then A19: HBB is open by TSEP_1:9;

|.(hq - hq).| = 0 by TOPRNS_1:28;

then hq in BB by A15;

then p in HBB by FUNCT_1:def 7, A13, A4, A9, A7;

then A20: p in Int HBB by A19, TOPS_1:23;

A21: M | hBBM = (M | (Int M)) | HBB by A1, PRE_TOPC:7;

rng h = [#] (Tball ((0. (TOP-REAL n)),1)) by A3, TOPS_2:def 5;

then h .: hBB = BB by FUNCT_1:77;

then A22: (Tball ((0. (TOP-REAL n)),1)) | (h .: hBB) = (TOP-REAL n) | (Ball (hq,s)) by A11, PRE_TOPC:7;

reconsider HBB = HBB as a_neighborhood of p by A20, CONNSP_2:def 1;

A23: (M | U) | hBB = M | hBBM by A7, PRE_TOPC:7;

then reconsider hh = h | hBB as Function of ((M | (Int M)) | HBB),((TOP-REAL n) | (Ball (hq,s))) by A22, JORDAN24:12, A21;

hh is being_homeomorphism by A3, A22, A23, A21, METRIZTS:2;

then A24: (M | (Int M)) | HBB, Tball (hq,s) are_homeomorphic by T_0TOPSP:def 1;

take HBB ; :: thesis: (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

Tball (hq,s), Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A15, Th3;

hence (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A15, A24, BORSUK_3:3; :: thesis: verum

end;p in Int M by A1;

then reconsider q = p as Point of M ;

consider U being a_neighborhood of q such that

A2: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1, Def7;

set MU = M | U;

set TR = TOP-REAL n;

consider h being Function of (M | U),(Tball ((0. (TOP-REAL n)),1)) such that

A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

A4: Int U c= U by TOPS_1:16;

A5: (Int M) /\ (Int U) in the topology of M by PRE_TOPC:def 2;

A6: Int U c= U by TOPS_1:16;

A7: [#] (M | U) = U by PRE_TOPC:def 5;

(Int U) /\ (Int M) c= Int U by XBOOLE_1:17;

then reconsider UIM = (Int M) /\ (Int U) as Subset of (M | U) by A6, A7, XBOOLE_1:1;

A8: h " (h .: UIM) c= UIM by A3, FUNCT_1:82;

A9: dom h = [#] (M | U) by A3, TOPS_2:def 5;

A11: [#] (Tball ((0. (TOP-REAL n)),1)) = Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider hum = h .: UIM as Subset of (TOP-REAL n) by XBOOLE_1:1;

UIM /\ ([#] (M | U)) = UIM by XBOOLE_1:28;

then UIM in the topology of (M | U) by A5, PRE_TOPC:def 4;

then UIM is open by PRE_TOPC:def 2;

then h .: UIM is open by A3, TOPGRP_1:25;

then hum is open by TSEP_1:9, A11;

then A12: Int hum = hum by TOPS_1:23;

A13: q in Int U by CONNSP_2:def 1;

then A14: q in UIM by A1, XBOOLE_0:def 4;

then h . q in hum by A9, FUNCT_1:def 6;

then reconsider hq = h . q as Point of (TOP-REAL n) ;

reconsider HQ = hq as Point of (Euclid n) by EUCLID:67;

h . q in h .: UIM by A14, A9, FUNCT_1:def 6;

then consider s being Real such that

A15: s > 0 and

A16: Ball (HQ,s) c= hum by A12, GOBOARD6:5;

A17: Ball (HQ,s) = Ball (hq,s) by TOPREAL9:13;

then reconsider BB = Ball (hq,s) as Subset of (Tball ((0. (TOP-REAL n)),1)) by A16, XBOOLE_1:1;

BB is open by TSEP_1:9;

then reconsider hBB = h " BB as open Subset of (M | U) by A3, TOPGRP_1:26;

hBB c= h " (h .: UIM) by A16, A17, RELAT_1:143;

then A18: hBB c= UIM by A8;

reconsider hBBM = hBB as Subset of M by A7, XBOOLE_1:1;

(Int U) /\ (Int M) c= Int M by XBOOLE_1:17;

then reconsider HBB = hBBM as Subset of (M | (Int M)) by A18, XBOOLE_1:1, A1;

hBBM is open by TSEP_1:9, A18;

then A19: HBB is open by TSEP_1:9;

|.(hq - hq).| = 0 by TOPRNS_1:28;

then hq in BB by A15;

then p in HBB by FUNCT_1:def 7, A13, A4, A9, A7;

then A20: p in Int HBB by A19, TOPS_1:23;

A21: M | hBBM = (M | (Int M)) | HBB by A1, PRE_TOPC:7;

rng h = [#] (Tball ((0. (TOP-REAL n)),1)) by A3, TOPS_2:def 5;

then h .: hBB = BB by FUNCT_1:77;

then A22: (Tball ((0. (TOP-REAL n)),1)) | (h .: hBB) = (TOP-REAL n) | (Ball (hq,s)) by A11, PRE_TOPC:7;

reconsider HBB = HBB as a_neighborhood of p by A20, CONNSP_2:def 1;

A23: (M | U) | hBB = M | hBBM by A7, PRE_TOPC:7;

then reconsider hh = h | hBB as Function of ((M | (Int M)) | HBB),((TOP-REAL n) | (Ball (hq,s))) by A22, JORDAN24:12, A21;

hh is being_homeomorphism by A3, A22, A23, A21, METRIZTS:2;

then A24: (M | (Int M)) | HBB, Tball (hq,s) are_homeomorphic by T_0TOPSP:def 1;

take HBB ; :: thesis: (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

Tball (hq,s), Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A15, Th3;

hence (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A15, A24, BORSUK_3:3; :: thesis: verum

b