set Y = TopStruct(# D,(cobool D) #);
reconsider Y' = TopStruct(# D,(cobool D) #) as anti-discrete TopStruct by TDLAT_3:def 2;
Y' is strict anti-discrete TopSpace ;
hence ( ADTS D is strict & ADTS D is anti-discrete & ADTS D is TopSpace-like ) ; :: thesis: verum