theorem Th21: :: TEX_2:21

for Y being non empty TopStruct
for A being Subset of Y st A = the carrier of Y holds
( A is discrete iff Y is discrete )