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

let X be Subset of M; :: thesis:
let p be Point of M; :: thesis:
assume A2: X = {p} ; :: thesis:
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 )

let x be object ; :: thesis:

hereby :: thesis:

assume x in V ; :: thesis:
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:

end;

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

end;

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

end;

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