:: deftheorem defines Cl MEASURE6:def 9 :
for X being real-membered set holds Cl X = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;