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

assume not X is almost_discrete ; :: thesis:
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:
thus ( C is boundary & C is closed ) by A3, A4; :: thesis:

end;