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 by Def4;
then (Cl (Int A)) ` = {} X by Th2;
then Int ((Int A) ` ) = {} X by TDLAT_3:4;
then Int (Cl (A ` )) = {} by TDLAT_3:3;
then Cl (A ` ) is boundary by TOPS_1:84;
hence A ` is nowhere_dense by TOPS_1:def 5; :: thesis: verum

end;

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:3;
then (Cl (Int A)) ` = {} X by TDLAT_3:4;
then Cl (Int A) = [#] X by Th2;
hence A is everywhere_dense by Def4; :: thesis: verum