theorem :: TDLAT_3:14

for Y being TopSpace-like TopStruct st bool the carrier of Y = {{}, the carrier of Y} holds
( Y is discrete & Y is anti-discrete )