theorem :: TDLAT_3:10

for Y being TopStruct st Y is discrete & Y is anti-discrete holds
bool the carrier of Y = {{}, the carrier of Y} ;