let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
let A be Subset of X; :: thesis: ( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
thus ( A is dense implies for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ) :: thesis: ( ( for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ) implies A is dense )

proof

assume A1: Cl A = the carrier of X ; :: according to TOPS_3:def 2 :: thesis: for C being Subset of X st A c= C & C is closed holds
C = the carrier of X
let C be Subset of X; :: thesis: ( A c= C & C is closed implies C = the carrier of X )
assume ( A c= C & C is closed ) ; :: thesis: C = the carrier of X
then Cl A c= C by TOPS_1:5;
hence C = the carrier of X by A1, XBOOLE_0:def 10; :: thesis: verum

end;

assume for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ; :: thesis: A is dense
then Cl A = the carrier of X by PRE_TOPC:18;
hence A is dense by Def2; :: thesis: verum