theorem Th10: :: TEX_4:10

for Y being non empty TopStruct
for x being Point of Y holds MaxADSF x is anti-discrete-set-family