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 () 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 () 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 () 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 () 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 () 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 () 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 () st U,B are_homeomorphic
consider U being a_neighborhood of p, S being open Subset of () such that
A2: U,S are_homeomorphic by A1;
consider U1 being open Subset of M, S being open Subset of () such that
A3: ( U1 c= U & p in U1 & U1,S are_homeomorphic ) by ;
reconsider U1 = U1 as non empty Subset of M by A3;
A4: M | U1,() | S are_homeomorphic by ;
consider f being Function of (M | U1),(() | S) such that
A5: f is being_homeomorphism by ;
A6: p in [#] (M | U1) by ;
reconsider S1 = () | S as non empty TopSpace by ;
reconsider M1 = M | U1 as non empty SubSpace of M ;
reconsider f = f as Function of M1,S1 ;
A7: [#] (() | S) = S by PRE_TOPC:def 5;
A8: [#] (() | S) c= [#] () by PRE_TOPC:def 4;
f . p in the carrier of (() | S) by ;
then reconsider q = f . p as Point of () by A8;
consider B being ball Subset of () such that
A9: ( B c= S & q in B ) by ;
reconsider B = B as non empty ball Subset of () by A9;
A10: f " is being_homeomorphism by ;
reconsider B1 = B as non empty Subset of S1 by A9, A7;
A11: rng f = [#] S1 by ;
A12: f is one-to-one by ;
A13: dom (f ") = the carrier of S1 by ;
then A14: (f ") . q in (f ") .: B1 by ;
reconsider U2 = (f ") .: B1 as non empty Subset of M1 by A13;
A15: dom ((f ") | B1) = B1 by ;
A16: dom ((f ") | B1) = [#] (S1 | B1) by
.= 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 ;
A17: g is being_homeomorphism by ;
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 ;
f is onto by ;
then f1 " = f " by ;
then A19: p1 in U2 by ;
A20: [#] M1 c= [#] M by PRE_TOPC:def 4;
reconsider V = U2 as Subset of M by ;
A21: B in the topology of () by PRE_TOPC:def 2;
B1 = B /\ ([#] S1) by XBOOLE_1:28;
then B1 in the topology of S1 by ;
then B1 is open by PRE_TOPC:def 2;
then (f ") .: B1 is open by ;
then reconsider V = V as a_neighborhood of p by ;
take V ; :: thesis: ex B being non empty ball Subset of () st V,B are_homeomorphic
take B ; :: thesis:
A22: M1 | U2,S1 | B1 are_homeomorphic by ;
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 ;
S1 | B1 = () | B by ;
hence V,B are_homeomorphic by ; :: thesis: verum