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