let n be Nat; :: thesis: for M being non empty TopSpace st ( for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ) holds

for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic

let M be non empty TopSpace; :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ) implies for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic )

assume A1: for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ; :: thesis: for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic

let p be Point of M; :: thesis: ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic

consider U being a_neighborhood of p, S being open Subset of (TOP-REAL n) such that

A2: U,S are_homeomorphic by A1;

consider U1 being open Subset of M, S being open Subset of (TOP-REAL n) such that

A3: ( U1 c= U & p in U1 & U1,S are_homeomorphic ) by A2, Th11;

reconsider U1 = U1 as non empty Subset of M by A3;

A4: M | U1,(TOP-REAL n) | S are_homeomorphic by A3, METRIZTS:def 1;

consider f being Function of (M | U1),((TOP-REAL n) | S) such that

A5: f is being_homeomorphism by T_0TOPSP:def 1, A3, METRIZTS:def 1;

A6: p in [#] (M | U1) by A3, PRE_TOPC:def 5;

reconsider S1 = (TOP-REAL n) | S as non empty TopSpace by A4, YELLOW14:18;

reconsider M1 = M | U1 as non empty SubSpace of M ;

reconsider f = f as Function of M1,S1 ;

A7: [#] ((TOP-REAL n) | S) = S by PRE_TOPC:def 5;

A8: [#] ((TOP-REAL n) | S) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

f . p in the carrier of ((TOP-REAL n) | S) by A6, FUNCT_2:5;

then reconsider q = f . p as Point of (TOP-REAL n) by A8;

consider B being ball Subset of (TOP-REAL n) such that

A9: ( B c= S & q in B ) by A6, A7, Th3, FUNCT_2:5;

reconsider B = B as non empty ball Subset of (TOP-REAL n) by A9;

A10: f " is being_homeomorphism by A5, TOPS_2:56;

reconsider B1 = B as non empty Subset of S1 by A9, A7;

A11: rng f = [#] S1 by A5, TOPS_2:def 5;

A12: f is one-to-one by A5, TOPS_2:def 5;

A13: dom (f ") = the carrier of S1 by A11, A12, TOPS_2:49;

then A14: (f ") . q in (f ") .: B1 by A9, FUNCT_1:def 6;

reconsider U2 = (f ") .: B1 as non empty Subset of M1 by A13;

A15: dom ((f ") | B1) = B1 by A13, RELAT_1:62;

A16: dom ((f ") | B1) = [#] (S1 | B1) by A15, PRE_TOPC:def 5

.= the carrier of (S1 | B1) ;

rng ((f ") | B1) = (f ") .: B1 by RELAT_1:115

.= [#] (M1 | U2) by PRE_TOPC:def 5

.= the carrier of (M1 | U2) ;

then reconsider g = (f ") | B1 as Function of (S1 | B1),(M1 | U2) by A16, FUNCT_2:1;

A17: g is being_homeomorphism by A10, METRIZTS:2;

reconsider p1 = p as Point of M1 by A6;

reconsider f1 = f as Function ;

A18: ( f1 is one-to-one & p in dom f1 ) by A5, A6, TOPS_2:def 5;

f is onto by A11, FUNCT_2:def 3;

then f1 " = f " by A12, TOPS_2:def 4;

then A19: p1 in U2 by A14, A18, FUNCT_1:34;

A20: [#] M1 c= [#] M by PRE_TOPC:def 4;

reconsider V = U2 as Subset of M by A20, XBOOLE_1:1;

A21: B in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

B1 = B /\ ([#] S1) by XBOOLE_1:28;

then B1 in the topology of S1 by A21, PRE_TOPC:def 4;

then B1 is open by PRE_TOPC:def 2;

then (f ") .: B1 is open by A10, TOPGRP_1:25;

then reconsider V = V as a_neighborhood of p by A19, CONNSP_2:3, CONNSP_2:9;

take V ; :: thesis: ex B being non empty ball Subset of (TOP-REAL n) st V,B are_homeomorphic

take B ; :: thesis: V,B are_homeomorphic

A22: M1 | U2,S1 | B1 are_homeomorphic by A17, T_0TOPSP:def 1;

rng (f ") c= [#] (M | U1) ;

then A23: rng (f ") c= U1 by PRE_TOPC:def 5;

(f ") .: B1 c= rng (f ") by RELAT_1:111;

then A24: M | V = M1 | U2 by A23, PRE_TOPC:7, XBOOLE_1:1;

S1 | B1 = (TOP-REAL n) | B by A9, PRE_TOPC:7;

hence V,B are_homeomorphic by A24, A22, METRIZTS:def 1; :: thesis: verum

for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic

let M be non empty TopSpace; :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ) implies for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic )

assume A1: for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ; :: thesis: for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic

let p be Point of M; :: thesis: ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic

consider U being a_neighborhood of p, S being open Subset of (TOP-REAL n) such that

A2: U,S are_homeomorphic by A1;

consider U1 being open Subset of M, S being open Subset of (TOP-REAL n) such that

A3: ( U1 c= U & p in U1 & U1,S are_homeomorphic ) by A2, Th11;

reconsider U1 = U1 as non empty Subset of M by A3;

A4: M | U1,(TOP-REAL n) | S are_homeomorphic by A3, METRIZTS:def 1;

consider f being Function of (M | U1),((TOP-REAL n) | S) such that

A5: f is being_homeomorphism by T_0TOPSP:def 1, A3, METRIZTS:def 1;

A6: p in [#] (M | U1) by A3, PRE_TOPC:def 5;

reconsider S1 = (TOP-REAL n) | S as non empty TopSpace by A4, YELLOW14:18;

reconsider M1 = M | U1 as non empty SubSpace of M ;

reconsider f = f as Function of M1,S1 ;

A7: [#] ((TOP-REAL n) | S) = S by PRE_TOPC:def 5;

A8: [#] ((TOP-REAL n) | S) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

f . p in the carrier of ((TOP-REAL n) | S) by A6, FUNCT_2:5;

then reconsider q = f . p as Point of (TOP-REAL n) by A8;

consider B being ball Subset of (TOP-REAL n) such that

A9: ( B c= S & q in B ) by A6, A7, Th3, FUNCT_2:5;

reconsider B = B as non empty ball Subset of (TOP-REAL n) by A9;

A10: f " is being_homeomorphism by A5, TOPS_2:56;

reconsider B1 = B as non empty Subset of S1 by A9, A7;

A11: rng f = [#] S1 by A5, TOPS_2:def 5;

A12: f is one-to-one by A5, TOPS_2:def 5;

A13: dom (f ") = the carrier of S1 by A11, A12, TOPS_2:49;

then A14: (f ") . q in (f ") .: B1 by A9, FUNCT_1:def 6;

reconsider U2 = (f ") .: B1 as non empty Subset of M1 by A13;

A15: dom ((f ") | B1) = B1 by A13, RELAT_1:62;

A16: dom ((f ") | B1) = [#] (S1 | B1) by A15, PRE_TOPC:def 5

.= the carrier of (S1 | B1) ;

rng ((f ") | B1) = (f ") .: B1 by RELAT_1:115

.= [#] (M1 | U2) by PRE_TOPC:def 5

.= the carrier of (M1 | U2) ;

then reconsider g = (f ") | B1 as Function of (S1 | B1),(M1 | U2) by A16, FUNCT_2:1;

A17: g is being_homeomorphism by A10, METRIZTS:2;

reconsider p1 = p as Point of M1 by A6;

reconsider f1 = f as Function ;

A18: ( f1 is one-to-one & p in dom f1 ) by A5, A6, TOPS_2:def 5;

f is onto by A11, FUNCT_2:def 3;

then f1 " = f " by A12, TOPS_2:def 4;

then A19: p1 in U2 by A14, A18, FUNCT_1:34;

A20: [#] M1 c= [#] M by PRE_TOPC:def 4;

reconsider V = U2 as Subset of M by A20, XBOOLE_1:1;

A21: B in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

B1 = B /\ ([#] S1) by XBOOLE_1:28;

then B1 in the topology of S1 by A21, PRE_TOPC:def 4;

then B1 is open by PRE_TOPC:def 2;

then (f ") .: B1 is open by A10, TOPGRP_1:25;

then reconsider V = V as a_neighborhood of p by A19, CONNSP_2:3, CONNSP_2:9;

take V ; :: thesis: ex B being non empty ball Subset of (TOP-REAL n) st V,B are_homeomorphic

take B ; :: thesis: V,B are_homeomorphic

A22: M1 | U2,S1 | B1 are_homeomorphic by A17, T_0TOPSP:def 1;

rng (f ") c= [#] (M | U1) ;

then A23: rng (f ") c= U1 by PRE_TOPC:def 5;

(f ") .: B1 c= rng (f ") by RELAT_1:111;

then A24: M | V = M1 | U2 by A23, PRE_TOPC:7, XBOOLE_1:1;

S1 | B1 = (TOP-REAL n) | B by A9, PRE_TOPC:7;

hence V,B are_homeomorphic by A24, A22, METRIZTS:def 1; :: thesis: verum