let Y be discrete TopStruct ; :: thesis: for A being Subset of holds the carrier of Y \ A in the topology of Y
let A be Subset of ; :: 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