theorem Th58: :: TEX_4:58

for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) } by Th41;