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. ()),1) are_homeomorphic
proof
let p be Point of (M | (Int M)); :: thesis: ex U being a_neighborhood of p st (M | (Int M)) | U, Tball ((0. ()),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. ()),1) are_homeomorphic by ;
set MU = M | U;
set TR = TOP-REAL n;
consider h being Function of (M | U),(Tball ((0. ()),1)) such that
A3: h is being_homeomorphism by ;
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 ;
A8: h " (h .: UIM) c= UIM by ;
A9: dom h = [#] (M | U) by ;
A11: [#] (Tball ((0. ()),1)) = Ball ((0. ()),1) by PRE_TOPC:def 5;
then reconsider hum = h .: UIM as Subset of () by XBOOLE_1:1;
UIM /\ ([#] (M | U)) = UIM by XBOOLE_1:28;
then UIM in the topology of (M | U) by ;
then UIM is open by PRE_TOPC:def 2;
then h .: UIM is open by ;
then hum is open by ;
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 ;
then h . q in hum by ;
then reconsider hq = h . q as Point of () ;
reconsider HQ = hq as Point of () by EUCLID:67;
h . q in h .: UIM by ;
then consider s being Real such that
A15: s > 0 and
A16: Ball (HQ,s) c= hum by ;
A17: Ball (HQ,s) = Ball (hq,s) by TOPREAL9:13;
then reconsider BB = Ball (hq,s) as Subset of (Tball ((0. ()),1)) by ;
BB is open by TSEP_1:9;
then reconsider hBB = h " BB as open Subset of (M | U) by ;
hBB c= h " (h .: UIM) by ;
then A18: hBB c= UIM by A8;
reconsider hBBM = hBB as Subset of M by ;
(Int U) /\ (Int M) c= Int M by XBOOLE_1:17;
then reconsider HBB = hBBM as Subset of (M | (Int M)) by ;
hBBM is open by ;
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 ;
then A20: p in Int HBB by ;
A21: M | hBBM = (M | (Int M)) | HBB by ;
rng h = [#] (Tball ((0. ()),1)) by ;
then h .: hBB = BB by FUNCT_1:77;
then A22: (Tball ((0. ()),1)) | (h .: hBB) = () | (Ball (hq,s)) by ;
reconsider HBB = HBB as a_neighborhood of p by ;
A23: (M | U) | hBB = M | hBBM by ;
then reconsider hh = h | hBB as Function of ((M | (Int M)) | HBB),(() | (Ball (hq,s))) by ;
hh is being_homeomorphism by ;
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. ()),1) are_homeomorphic
Tball (hq,s), Tball ((0. ()),1) are_homeomorphic by ;
hence (M | (Int M)) | HBB, Tball ((0. ()),1) are_homeomorphic by ; :: thesis: verum
end;
hence for b1 being non empty TopSpace st b1 = M | (Int M) holds
b1 is n -locally_euclidean by Th13; :: thesis: verum