theorem Th1: :: TEX_4:1

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