begin
begin
Lm1:
for n being Nat
for M being non empty TopSpace st M is n -locally_euclidean 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
set T = (TOP-REAL 0) | ([#] (TOP-REAL 0));
Lm2:
(TOP-REAL 0) | ([#] (TOP-REAL 0)) = TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #)
by TSEP_1:93;