let M be non empty locally_euclidean TopSpace; :: thesis: for p being Point of (M | (Int M)) ex U being a_neighborhood of p ex n being Nat st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
set MI = M | (Int M);
let p be Point of (M | (Int M)); :: thesis: ex U being a_neighborhood of p ex n being Nat st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
A1: [#] (M | (Int M)) = Int M by PRE_TOPC:def 5;
then p in Int M ;
then reconsider q = p as Point of M ;
consider U being a_neighborhood of q, n being Nat such that
A2: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1, Def4;
A3: Int U c= U by TOPS_1:16;
A4: (Int M) /\ (Int U) in the topology of M by PRE_TOPC:def 2;
A5: Int U c= U by TOPS_1:16;
set MU = M | U;
set TR = TOP-REAL n;
consider h being Function of (M | U),(Tball ((0. (TOP-REAL n)),1)) such that
A6: h is being_homeomorphism by A2, T_0TOPSP:def 1;
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 A5, A7, XBOOLE_1:1;
A8: dom h = [#] (M | U) by A6, TOPS_2:def 5;
A10: [#] (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 A4, PRE_TOPC:def 4;
then UIM is open by PRE_TOPC:def 2;
then h .: UIM is open by A6, TOPGRP_1:25;
then hum is open by TSEP_1:9, A10;
then A11: Int hum = hum by TOPS_1:23;
A12: h " (h .: UIM) c= UIM by A6, FUNCT_1:82;
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 A8, 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, A8, FUNCT_1:def 6;
then consider s being Real such that
A15: s > 0 and
A16: Ball (HQ,s) c= hum by A11, 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 A6, TOPGRP_1:26;
hBB c= h " (h .: UIM) by A16, A17, RELAT_1:143;
then A18: hBB c= UIM by A12;
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;
A20: M | hBBM = (M | (Int M)) | HBB by A1, PRE_TOPC:7;
rng h = [#] (Tball ((0. (TOP-REAL n)),1)) by A6, TOPS_2:def 5;
then h .: hBB = BB by FUNCT_1:77;
then A21: (Tball ((0. (TOP-REAL n)),1)) | (h .: hBB) = (TOP-REAL n) | (Ball (hq,s)) by A10, PRE_TOPC:7;
|.(hq - hq).| = 0 by TOPRNS_1:28;
then hq in BB by A15;
then p in HBB by FUNCT_1:def 7, A13, A3, A8, A7;
then p in Int HBB by A19, TOPS_1:23;
then reconsider HBB = HBB as a_neighborhood of p by CONNSP_2:def 1;
A22: (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 A21, JORDAN24:12, A20;
hh is being_homeomorphism by A6, A21, A22, A20, METRIZTS:2;
then A23: (M | (Int M)) | HBB, Tball (hq,s) are_homeomorphic by T_0TOPSP:def 1;
take HBB ; :: thesis: ex n being Nat st (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 ex n being Nat st (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A15, A23, BORSUK_3:3; :: thesis: verum