let X be TopSpace; :: thesis: ( X is anti-discrete iff for A being Subset of X holds
( not A is closed or A = {} or A = the carrier of X ) )
thus ( X is anti-discrete implies for A being Subset of X holds
( not A is closed or A = {} or A = the carrier of X ) ) :: thesis: ( ( for A being Subset of X holds
( not A is closed or A = {} or A = the carrier of X ) ) implies X is anti-discrete )
proof
assume A1: X is anti-discrete ; :: 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 ` = {} or A ` = the carrier of X ) by A1, Th18;
then ( (A `) ` = [#] X or (A `) ` = {} X ) by XBOOLE_1:37;
hence ( A = {} or A = the carrier of X ) ; :: thesis: verum
end;
assume A2: for A being Subset of X holds
( not A is closed or A = {} or A = the carrier of X ) ; :: thesis: X is anti-discrete
now :: thesis: for B being Subset of X holds
( not B is open or B = {} or B = the carrier of X )
let B be Subset of X; :: thesis: ( not B is open or B = {} or B = the carrier of X )
assume B is open ; :: thesis: ( B = {} or B = the carrier of X )
then ( B ` = {} or B ` = the carrier of X ) by A2;
then ( (B `) ` = [#] X or (B `) ` = {} X ) by XBOOLE_1:37;
hence ( B = {} or B = the carrier of X ) ; :: thesis: verum
end;
hence X is anti-discrete by Th18; :: thesis: verum