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