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 ;
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 ;
Cl {a} is open by ;
then Cl {x} misses Cl {a} by ;
hence contradiction by A4, A7, XBOOLE_0:3; :: thesis: verum
end;
assume A = {x} ; :: thesis: A is closed
hence A is closed by ; :: thesis: verum
end;
hence Y is discrete by ; :: thesis: verum