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