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 Th16; :: 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 by A2, A1, Th22;
hence X is discrete by Th17; :: thesis: verum