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

proof

assume A1: X is discrete ; :: thesis: for A being Subset of X holds A is closed
let A be Subset of X; :: thesis: A is closed
A ` is open by A1, Th15;
hence A is closed by TOPS_1:3; :: thesis: verum

end;

assume A2: for A being Subset of X holds A is closed ; :: thesis: X is discrete

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

let A be Subset of X; :: thesis: A is open
A ` is closed by A2;
hence A is open by TOPS_1:4; :: thesis: verum

end;

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