let X be non empty TopSpace; :: thesis: ( ( for A being Subset of X st A <> the carrier of X holds
A is boundary ) implies X is anti-discrete )
assume A1: for A being Subset of X st A <> the carrier of X holds
A is boundary ; :: thesis: X is anti-discrete

now :: thesis: for A being Subset of X st A <> the carrier of X holds
Int A = {}

let A be Subset of X; :: thesis: ( A <> the carrier of X implies Int A = {} )
reconsider B = A as Subset of X ;
assume A <> the carrier of X ; :: thesis: Int A = {}
then B is boundary by A1;
hence Int A = {} ; :: thesis: verum

end;

hence X is anti-discrete by Th12; :: thesis: verum