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

proof

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

end;

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