let X be TopSpace; :: thesis: ( X is discrete iff ( X is almost_discrete & ( for A being Subset of X
for x being Point of X st A = {x} holds
A is closed ) ) )
thus ( X is discrete implies ( X is almost_discrete & ( for A being Subset of X
for x being Point of X st A = {x} holds
A is closed ) ) ) by Th18; :: thesis: ( X is almost_discrete & ( for A being Subset of X
for x being Point of X st A = {x} holds
A is closed ) implies X is discrete )
assume A1: X is almost_discrete ; :: thesis: ( ex A being Subset of X ex x being Point of X st
( A = {x} & not A is closed ) or X is discrete )
assume A2: for A being Subset of X
for x being Point of X st A = {x} holds
A is closed ; :: thesis: X is discrete
for A being Subset of X
for x being Point of X st A = {x} holds
A is open

proof

let A be Subset of X; :: thesis: for x being Point of X st A = {x} holds
A is open
let x be Point of X; :: thesis: ( A = {x} implies A is open )
assume A = {x} ; :: thesis: A is open
then A is closed by A2;
hence A is open by A1, Th24; :: thesis: verum

end;

hence X is discrete by Th19; :: thesis: verum