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

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

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

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

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

end;

hence contradiction by A1; :: thesis: verum

end;

assume A4: for C being Subset of X st C <> the carrier of X holds
not C is dense ; :: thesis: X is discrete
assume not X is discrete ; :: thesis: contradiction
then consider A being non empty Subset of X such that
A5: A is boundary ;

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

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

end;

hence contradiction by A4; :: thesis: verum