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