let M be non empty TopSpace; :: thesis: ( M is 0 -locally_euclidean implies M is discrete )
assume A1: M is 0 -locally_euclidean ; :: thesis: M is discrete
for X being Subset of M
for p being Point of M st X = {p} holds
X is open

proof

let X be Subset of M; :: thesis: for p being Point of M st X = {p} holds
X is open
let p be Point of M; :: thesis: ( X = {p} implies X is open )
assume A2: X = {p} ; :: thesis: X is open
consider U being a_neighborhood of p such that
A3: U, [#] (TOP-REAL 0) are_homeomorphic by A1, Th13;
A4: Int U c= U by TOPS_1:16;
A5: p in U by A4, CONNSP_2:def 1;
consider f being Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) such that
A6: f is being_homeomorphism by T_0TOPSP:def 1, A3, METRIZTS:def 1;
consider V being Subset of M such that
A7: ( V is open & V c= U & p in V ) by CONNSP_2:6;
for x being object holds
( x in V iff x = p )

proof

let x be object ; :: thesis: ( x in V iff x = p )

hereby :: thesis: ( x = p implies x in V )

assume x in V ; :: thesis: x = p
then A8: x in U by A7;
A9: f is one-to-one by A6, TOPS_2:def 5;
x in [#] (M | U) by A8, PRE_TOPC:def 5;
then A10: x in dom f by A6, TOPS_2:def 5;
then A11: f . x in rng f by FUNCT_1:3;
p in [#] (M | U) by A5, PRE_TOPC:def 5;
then A12: p in dom f by A6, TOPS_2:def 5;
then A13: f . p in rng f by FUNCT_1:3;
f . x = 0. (TOP-REAL 0) by Lm2, A11
.= f . p by Lm2, A13 ;
hence x = p by A9, A10, A12; :: thesis: verum

end;

assume x = p ; :: thesis: x in V
hence x in V by A7; :: thesis: verum

end;

hence X is open by A2, A7, TARSKI:def 1; :: thesis: verum

end;

hence M is discrete by TDLAT_3:17; :: thesis: verum