let T be TopSpace; :: thesis: for A being Subset of T holds
( Cl A <> {} iff A <> {} )
let A be Subset of T; :: thesis: ( Cl A <> {} iff A <> {} )
( A <> {} implies Cl A <> {} )

proof

set x = the Element of A;
A1: A c= Cl A by PRE_TOPC:18;
assume A2: A <> {} ; :: thesis: Cl A <> {}
ex x being set st x in Cl A

proof

take the Element of A ; :: thesis: the Element of A in Cl A
thus the Element of A in Cl A by A2, A1; :: thesis: verum

end;

hence Cl A <> {} ; :: thesis: verum

end;

hence ( Cl A <> {} iff A <> {} ) by PRE_TOPC:22; :: thesis: verum