let X be non empty TopSpace; :: thesis: ( ( for A being Subset of X st not A is empty holds
Cl A = the carrier of X ) implies X is anti-discrete )
assume A1: for A being Subset of X st not A is empty holds
Cl A = the carrier of X ; :: thesis: X is anti-discrete
now :: thesis: for A being Subset of X holds
( not A is closed or A = {} or A = the carrier of X )
let A be Subset of X; :: thesis: ( not A is closed or A = {} or A = the carrier of X )
assume A is closed ; :: thesis: ( A = {} or A = the carrier of X )
then A = Cl A by PRE_TOPC:22;
hence ( A = {} or A = the carrier of X ) by A1; :: thesis: verum
end;
hence X is anti-discrete by TDLAT_3:19; :: thesis: verum