thus ( A is nowhere_dense implies Int (Cl A) = {} ) :: thesis: ( Int (Cl A) = {} implies A is nowhere_dense )

proof

assume A is nowhere_dense ; :: thesis: Int (Cl A) = {}
then Cl A is boundary by TOPS_1:def 5;
hence Int (Cl A) = {} ; :: thesis: verum

end;

assume Int (Cl A) = {} ; :: thesis: A is nowhere_dense
then Cl A is boundary by Def1;
hence A is nowhere_dense by TOPS_1:def 5; :: thesis: verum