theorem Th39: :: TEX_4:39

for Y being non empty TopSpace
for A being Subset of Y holds MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }