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 and
A2: A is closed by Th33;
take A ` ; :: thesis: ( A ` <> the carrier of X & A ` is dense & A ` is open )
thus ( A ` <> the carrier of X & A ` is dense & A ` is open ) by A1, A2, TOPS_3:1; :: thesis: verum
end;
given A being Subset of X such that A3: A <> the carrier of X and
A4: A is dense and
A5: A is open ; :: thesis: not X is almost_discrete
now :: thesis: ex B being non empty Subset of X st
( B is boundary & B is closed )
reconsider B = A ` as non empty Subset of X by A3, TOPS_3:2;
take B = B; :: thesis: ( B is boundary & B is closed )
thus ( B is boundary & B is closed ) by A4, A5, TOPS_3:18; :: thesis: verum
end;
hence not X is almost_discrete ; :: thesis: verum