theorem Th55: :: TEX_4:55
for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } by Th39;