:: deftheorem defines open PDIFF_7:def 3 :
for m being non zero Nat
for X being Subset of (REAL m) holds
( X is open iff ex X0 being Subset of (REAL-NS m) st
( X0 = X & X0 is open ) );