theorem Th20: :: TEX_4:20

for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x is maximal_anti-discrete