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

proof

assume A1: X is almost_discrete ; :: thesis: for A being Subset of X st A is open holds
Cl A = A
let A be Subset of X; :: thesis: ( A is open implies Cl A = A )
assume A is open ; :: thesis: Cl A = A
then A is closed by A1, Th23;
hence Cl A = A by PRE_TOPC:52; :: thesis: verum

end;

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

now

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

end;

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