theorem Th16: :: TEX_4:16

for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & A is open holds
A is maximal_anti-discrete