let Y be anti-discrete TopStruct ; :: thesis: for A being Subset of Y st A in the topology of Y holds
the carrier of Y \ A in the topology of Y
let A be Subset of Y; :: thesis: ( A in the topology of Y implies the carrier of Y \ A in the topology of Y )
A1: the topology of Y = {{}, the carrier of Y} by Def2;
assume A in the topology of Y ; :: thesis: the carrier of Y \ A in the topology of Y
then ( A = {} or A = the carrier of Y ) by A1, TARSKI:def 2;
then ( the carrier of Y \ A = the carrier of Y or the carrier of Y \ A = {} ) by XBOOLE_1:37;
hence the carrier of Y \ A in the topology of Y by A1, TARSKI:def 2; :: thesis: verum