let Y be non empty TopStruct ; :: thesis: for A being empty Subset of holds A is anti-discrete
let A be empty Subset of ; :: thesis: A is anti-discrete
for G being Subset of 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