for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )