theorem Th11: :: TDLAT_3:11
for Y being TopStruct st {} in the topology of Y & the carrier of Y in the topology of Y & bool the carrier of Y = {{}, the carrier of Y} holds
( Y is discrete & Y is anti-discrete )