let Y be discrete TopStruct ; :: thesis: for A being Subset of Y holds the carrier of Y \ A in the topology of Y
let A be Subset of Y; :: thesis: the carrier of Y \ A in the topology of Y
the topology of Y = bool the carrier of Y by Def1;
hence the carrier of Y \ A in the topology of Y ; :: thesis: verum