let X be non empty TopSpace; :: thesis: ( not X is almost_discrete iff ex A being non empty Subset of X st
( A is boundary & A is closed ) )
thus ( not X is almost_discrete implies ex A being non empty Subset of X st
( A is boundary & A is closed ) ) :: thesis: ( ex A being non empty Subset of X st
( A is boundary & A is closed ) implies not X is almost_discrete )

proof

assume not X is almost_discrete ; :: thesis: ex A being non empty Subset of X st
( A is boundary & A is closed )
then consider A being non empty Subset of X such that
A1: A is nowhere_dense ;
consider C being Subset of X such that
A2: A c= C and
A3: C is closed and
A4: C is boundary by A1, TOPS_3:27;
reconsider C = C as non empty Subset of X by A2;
reconsider C = C as non empty Subset of X ;
take C ; :: thesis: ( C is boundary & C is closed )
thus ( C is boundary & C is closed ) by A3, A4; :: thesis: verum

end;

given A being non empty Subset of X such that A5: A is boundary and
A6: A is closed ; :: thesis: not X is almost_discrete
thus not X is almost_discrete by A5, A6; :: thesis: verum