let n be Nat; 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; ( ( 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 ( ( 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
(
M is
without_boundary &
M is
n -locally_euclidean )
;
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;
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;
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;
verum
end;
assume A6:
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 )
now 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 let p be
Point of
M;
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;
ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic take S =
S;
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;
verum end;
hence
( M is without_boundary & M is n -locally_euclidean )
by Def4; verum