:: deftheorem defines closed MEASURE6:def 7 :
for R being Subset-Family of REAL holds
( R is closed iff for X being Subset of REAL st X in R holds
X is closed );