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;