for X being non empty TopSpace
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 ) by TOPS_1:5, PRE_TOPC:18;