:: deftheorem defines closed COMPL_SP:def 4 :
for M being MetrStruct
for A being Subset of M holds
( A is closed iff A ` is open );