:: deftheorem defines open COMPL_SP:def 3 :
for M being MetrStruct
for U being Subset of M holds
( U is open iff U in Family_open_set M );