let X be TopSpace; :: thesis: ( X is anti-discrete iff for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) )
A1: the carrier of X in the topology of X by PRE_TOPC:def 1;
thus ( X is anti-discrete implies for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) ) :: thesis: ( ( for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) ) implies X is anti-discrete )
proof
assume A2: X is anti-discrete ; :: thesis: for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X )
let A be Subset of X; :: thesis: ( not A is open or A = {} or A = the carrier of X )
assume A is open ; :: thesis: ( A = {} or A = the carrier of X )
then A in the topology of X by PRE_TOPC:def 2;
then A in {{}, the carrier of X} by A2;
hence ( A = {} or A = the carrier of X ) by TARSKI:def 2; :: thesis: verum
end;
assume A3: for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) ; :: thesis: X is anti-discrete
now :: thesis: for P being object st P in the topology of X holds
P in {{}, the carrier of X}
let P be object ; :: thesis: ( P in the topology of X implies P in {{}, the carrier of X} )
assume A4: P in the topology of X ; :: thesis: P in {{}, the carrier of X}
then reconsider C = P as Subset of X ;
C is open by A4, PRE_TOPC:def 2;
then ( C = {} or C = the carrier of X ) by A3;
hence P in {{}, the carrier of X} by TARSKI:def 2; :: thesis: verum
end;
then A5: the topology of X c= {{}, the carrier of X} ;
{} in the topology of X by PRE_TOPC:1;
then {{}, the carrier of X} c= the topology of X by A1, ZFMISC_1:32;
then the topology of X = {{}, the carrier of X} by A5;
hence X is anti-discrete ; :: thesis: verum