:: deftheorem defines closed DUALSP04:def 4 :
for X being RealUnitarySpace
for Y being Subset of X holds
( Y is closed iff ex Z being Subset of (RUSp2RNSp X) st
( Z = Y & Z is closed ) );