let n be Nat; :: thesis: for M being non empty TopSpace holds

( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )

let M be non empty TopSpace; :: thesis: ( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )

( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )

let M be non empty TopSpace; :: thesis: ( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )

hereby :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ) implies ( M is without_boundary & M is n -locally_euclidean ) )

assume A6:
for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
; :: thesis: ( M is without_boundary & M is n -locally_euclidean )assume
( M is without_boundary & M is n -locally_euclidean )
; :: thesis: for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic

then AA: 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 by Def4;

let p be Point of M; :: thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic

consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that

A2: U,B are_homeomorphic by Lm1, AA;

take U = U; :: thesis: U, [#] (TOP-REAL n) are_homeomorphic

A3: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

reconsider B1 = (TOP-REAL n) | B as non empty TopSpace ;

M | U,B1 are_homeomorphic by A2, METRIZTS:def 1;

then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;

A4: U1,B1 are_homeomorphic by A2, METRIZTS:def 1;

B1, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by Th10, A3, METRIZTS:def 1;

hence U, [#] (TOP-REAL n) are_homeomorphic by A3, METRIZTS:def 1, A4, BORSUK_3:3; :: thesis: verum

end;then AA: 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 by Def4;

let p be Point of M; :: thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic

consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that

A2: U,B are_homeomorphic by Lm1, AA;

take U = U; :: thesis: U, [#] (TOP-REAL n) are_homeomorphic

A3: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

reconsider B1 = (TOP-REAL n) | B as non empty TopSpace ;

M | U,B1 are_homeomorphic by A2, METRIZTS:def 1;

then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;

A4: U1,B1 are_homeomorphic by A2, METRIZTS:def 1;

B1, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by Th10, A3, METRIZTS:def 1;

hence U, [#] (TOP-REAL n) are_homeomorphic by A3, METRIZTS:def 1, A4, BORSUK_3:3; :: thesis: verum

now :: 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

hence
( M is without_boundary & M is n -locally_euclidean )
by Def4; :: thesis: verumlet p be Point of M; :: thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

consider U being a_neighborhood of p such that

A7: U, [#] (TOP-REAL n) are_homeomorphic by A6;

set S = the non empty ball Subset of (TOP-REAL n);

reconsider S = the non empty ball Subset of (TOP-REAL n) as open Subset of (TOP-REAL n) ;

take U = U; :: thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

take S = S; :: thesis: U,S are_homeomorphic

A9: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

A10: M | U, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A7, A9, METRIZTS:def 1;

then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;

reconsider S1 = (TOP-REAL n) | S as non empty TopSpace ;

A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),S1 are_homeomorphic by Th10, A9, METRIZTS:def 1;

U1,S1 are_homeomorphic by A10, A11, BORSUK_3:3;

hence U,S are_homeomorphic by METRIZTS:def 1; :: thesis: verum

end;consider U being a_neighborhood of p such that

A7: U, [#] (TOP-REAL n) are_homeomorphic by A6;

set S = the non empty ball Subset of (TOP-REAL n);

reconsider S = the non empty ball Subset of (TOP-REAL n) as open Subset of (TOP-REAL n) ;

take U = U; :: thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

take S = S; :: thesis: U,S are_homeomorphic

A9: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

A10: M | U, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A7, A9, METRIZTS:def 1;

then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;

reconsider S1 = (TOP-REAL n) | S as non empty TopSpace ;

A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),S1 are_homeomorphic by Th10, A9, METRIZTS:def 1;

U1,S1 are_homeomorphic by A10, A11, BORSUK_3:3;

hence U,S are_homeomorphic by METRIZTS:def 1; :: thesis: verum