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

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

hence
Y is discrete
by A1, TDLAT_3:26; :: thesis: verum
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;

hence A is closed by A2, A3, XBOOLE_0:def 10; :: thesis: verum

end;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
A = {x}
; :: thesis: A is closed 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;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

hence A is closed by A2, A3, XBOOLE_0:def 10; :: thesis: verum