let X be TopSpace; :: thesis: ( X is almost_discrete iff for A being Subset of X st A is closed holds
Int A = A )
thus ( X is almost_discrete implies for A being Subset of X st A is closed holds
Int A = A ) by Th22, TOPS_1:23; :: thesis: ( ( for A being Subset of X st A is closed holds
Int A = A ) implies X is almost_discrete )
assume A1: for A being Subset of X st A is closed holds
Int A = A ; :: thesis: X is almost_discrete

now :: 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 Int A = A by A1;
hence A is open ; :: thesis: verum

end;

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