theorem Th16: :: TDLAT_3:16

for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is closed )