let X be non empty TopSpace; :: thesis: ( not X is almost_discrete iff ex A being Subset of X st
( A <> the carrier of X & A is dense & A is open ) )
thus ( not X is almost_discrete implies ex A being Subset of X st
( A <> the carrier of X & A is dense & A is open ) ) :: thesis: ( ex A being Subset of X st
( A <> the carrier of X & A is dense & A is open ) implies not X is almost_discrete )

proof

assume not X is almost_discrete ; :: thesis: ex A being Subset of X st
( A <> the carrier of X & A is dense & A is open )
then consider A being non empty Subset of X such that
A1: ( A is boundary & A is closed ) by Th37;
take B = A ` ; :: thesis: ( B <> the carrier of X & B is dense & B is open )
thus ( B <> the carrier of X & B is dense & B is open ) by A1, TOPS_3:1; :: thesis: verum

end;

given A being Subset of X such that A2: A <> the carrier of X and
A3: ( A is dense & A is open ) ; :: thesis: not X is almost_discrete

now

reconsider B = A ` as non empty Subset of X by A2, TOPS_3:2;
take B = B; :: thesis: ( B is boundary & B is closed )
thus ( B is boundary & B is closed ) by A3, TOPS_3:18; :: thesis: verum

end;

hence not X is almost_discrete by Th37; :: thesis: verum