let X be TopSpace; :: thesis: ( X is almost_discrete iff for A being Subset of X st A is closed holds
A is open )
thus ( X is almost_discrete implies for A being Subset of X st A is closed holds
A is open ) :: thesis: ( ( for A being Subset of X st A is closed holds
A is open ) implies X is almost_discrete )

proof

assume A1: X is almost_discrete ; :: thesis: for A being Subset of X st A is closed holds
A is open
let A be Subset of X; :: thesis: ( A is closed implies A is open )
assume A is closed ; :: thesis: A is open
then A ` is closed by A1, Th21;
hence A is open by TOPS_1:4; :: thesis: verum

end;

assume A2: for A being Subset of X st A is closed holds
A is open ; :: thesis: X is almost_discrete

now :: thesis: for A being Subset of X st A is open holds
A is closed

let A be Subset of X; :: thesis: ( A is open implies A is closed )
assume A is open ; :: thesis: A is closed
then A ` is open by A2;
hence A is closed by TOPS_1:3; :: thesis: verum

end;

hence X is almost_discrete by Th21; :: thesis: verum