let X be non empty anti-discrete TopSpace; :: thesis: for A being Subset of X holds
( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) )
let A be Subset of X; :: thesis: ( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) )
thus ( A <> the carrier of X implies Int A = {} ) :: thesis: ( A = the carrier of X implies Int A = the carrier of X )

proof

assume A1: A <> the carrier of X ; :: thesis: Int A = {}

now :: thesis: not Int A = the carrier of X

assume Int A = the carrier of X ; :: thesis: contradiction
then the carrier of X c= A by TOPS_1:16;
hence contradiction by A1, XBOOLE_0:def 10; :: thesis: verum

end;

hence Int A = {} by TDLAT_3:18; :: thesis: verum

end;

thus ( A = the carrier of X implies Int A = the carrier of X ) :: thesis: verum

proof

assume A = the carrier of X ; :: thesis: Int A = the carrier of X
then A = [#] X ;
hence Int A = the carrier of X by TOPS_1:15; :: thesis: verum

end;