let Y be non empty TopStruct ; :: thesis: for A being empty Subset of Y holds A is anti-discrete
let A be empty Subset of Y; :: thesis: A is anti-discrete
for G being Subset of Y holds
( not G is open or A misses G or A c= G ) by XBOOLE_1:65;
hence A is anti-discrete by Def3; :: thesis: verum