A14:
[#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) = {(0. (TOP-REAL 0))}
by Lm2, EUCLID:22, EUCLID:77;
let M be non empty TopSpace; ( M is discrete implies M is 0 -locally_euclidean )
assume A15:
M is discrete
; M is 0 -locally_euclidean
for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic
proof
let p be
Point of
M;
ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic
reconsider U =
{p} as
Subset of
M by ZFMISC_1:31;
A16:
(
U is
open &
p in U )
by A15, TARSKI:def 1, TDLAT_3:15;
then reconsider U =
U as
a_neighborhood of
p by CONNSP_2:3;
take
U
;
U, [#] (TOP-REAL 0) are_homeomorphic
set f =
{[p,(0. (TOP-REAL 0))]};
A17:
p in [#] (M | U)
by A16, PRE_TOPC:def 5;
A19:
dom {[p,(0. (TOP-REAL 0))]} = U
by RELAT_1:9;
then A20:
dom {[p,(0. (TOP-REAL 0))]} = [#] (M | U)
by PRE_TOPC:def 5;
then reconsider f =
{[p,(0. (TOP-REAL 0))]} as
Function of
(M | U),
((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A17, Lm2, ZFMISC_1:87, FUNCT_2:def 1, ZFMISC_1:31;
A21:
rng f = [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0)))
by A14, RELAT_1:9;
for
P being
Subset of
(M | U) holds
(
P is
closed iff
f .: P is
closed )
then
M | U,
(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic
by T_0TOPSP:def 1, A20, A21, TOPS_2:58;
hence
U,
[#] (TOP-REAL 0) are_homeomorphic
by METRIZTS:def 1;
verum
end;
hence
M is 0 -locally_euclidean
by Th13; verum