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

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

proof

take x ; :: thesis: x in Cl A
thus x in Cl A by A2, A1, TARSKI:def 3; :: thesis: verum

end;

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

end;

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