let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is everywhere_dense iff A ` is nowhere_dense )
let A be Subset of X; :: thesis: ( A is everywhere_dense iff A ` is nowhere_dense )
thus ( A is everywhere_dense implies A ` is nowhere_dense ) :: thesis: ( A ` is nowhere_dense implies A is everywhere_dense )

proof

assume A is everywhere_dense ; :: thesis: A ` is nowhere_dense
then Cl (Int A) = [#] X ;
then (Cl (Int A)) ` = {} X by Th2;
then Int ((Int A) `) = {} X by TDLAT_3:3;
then Int (Cl (A `)) = {} by TDLAT_3:2;
then Cl (A `) is boundary ;
hence A ` is nowhere_dense ; :: thesis: verum

end;

assume A ` is nowhere_dense ; :: thesis: A is everywhere_dense
then Cl (A `) is boundary ;
then Int (Cl (A `)) = {} X ;
then Int ((Int A) `) = {} X by TDLAT_3:2;
then (Cl (Int A)) ` = {} X by TDLAT_3:3;
then Cl (Int A) = [#] X by Th2;
hence A is everywhere_dense ; :: thesis: verum