theorem Th40: :: TEX_4:40

for Y being non empty TopStruct
for F, A being Subset of Y st F is closed & A c= F holds
MaxADSet A c= F