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