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

proof

assume A is dense ; :: thesis: A ` is boundary
then (A ` ) ` is dense ;
hence A ` is boundary by TOPS_1:def 4; :: thesis: verum

end;

assume A ` is boundary ; :: thesis: A is dense
then (A ` ) ` is dense by TOPS_1:def 4;
hence A is dense ; :: thesis: verum