let X be non empty TopSpace; :: thesis: ( X is almost_discrete iff for A being Subset of X st A <> the carrier of X holds
not A is everywhere_dense )

hereby :: thesis: ( ( for A being Subset of X st A <> the carrier of X holds
not A is everywhere_dense ) implies X is almost_discrete )

assume A1: X is almost_discrete ; :: thesis: for A being Subset of X st A <> the carrier of X holds
not A is everywhere_dense
assume ex A being Subset of X st
( A <> the carrier of X & A is everywhere_dense ) ; :: thesis: contradiction
then consider A being Subset of X such that
A2: A is everywhere_dense and
A3: A <> the carrier of X ;

now :: thesis: ex B being non empty Subset of X st B is nowhere_dense

reconsider B = A ` as non empty Subset of X by A3, TOPS_3:2;
take B = B; :: thesis: B is nowhere_dense
thus B is nowhere_dense by A2, TOPS_3:39; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum

end;

assume A4: for A being Subset of X st A <> the carrier of X holds
not A is everywhere_dense ; :: thesis: X is almost_discrete
assume not X is almost_discrete ; :: thesis: contradiction
then consider A being non empty Subset of X such that
A5: A is nowhere_dense ;

now :: thesis: ex B being Element of K10( the carrier of X) st
( B <> the carrier of X & B is everywhere_dense )

take B = A ` ; :: thesis: ( B <> the carrier of X & B is everywhere_dense )
thus ( B <> the carrier of X & B is everywhere_dense ) by A5, TOPS_3:1, TOPS_3:40; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum