:: deftheorem defines open NFCONT_1:def 4 :
for S being RealNormSpace
for X being Subset of S holds
( X is open iff X ` is closed );