let Y be non empty TopSpace; :: thesis: ( Y is almost_discrete & Y is T_0 implies Y is discrete )
assume A1: ( Y is almost_discrete & Y is T_0 ) ; :: thesis: Y is discrete
for A being Subset of Y
for x being Point of Y st A = {x} holds
A is closed

proof

let A be Subset of Y; :: thesis: for x being Point of Y st A = {x} holds
A is closed
let x be Point of Y; :: thesis: ( A = {x} implies A is closed )
x in Cl {x} by Lm2;
then A2: {x} c= Cl {x} by ZFMISC_1:31;

A3: now :: thesis: Cl {x} c= {x}

assume not Cl {x} c= {x} ; :: thesis: contradiction
then consider a being object such that
A4: a in Cl {x} and
A5: not a in {x} by TARSKI:def 3;
reconsider a = a as Point of Y by A4;
a <> x by A5, TARSKI:def 1;
then not x in Cl {a} by A1, A4;
then x in (Cl {a}) ` by SUBSET_1:29;
then {x} c= (Cl {a}) ` by ZFMISC_1:31;
then A6: {x} misses Cl {a} by SUBSET_1:23;
A7: ( a in {a} & {a} c= Cl {a} ) by PRE_TOPC:18, TARSKI:def 1;
Cl {a} is open by A1, TDLAT_3:22;
then Cl {x} misses Cl {a} by A6, TSEP_1:36;
hence contradiction by A4, A7, XBOOLE_0:3; :: thesis: verum

end;

assume A = {x} ; :: thesis: A is closed
hence A is closed by A2, A3, XBOOLE_0:def 10; :: thesis: verum

end;

hence Y is discrete by A1, TDLAT_3:26; :: thesis: verum