theorem Th31: :: PDIFF_7:31

for m being non zero Nat
for X being Subset of (REAL m) holds
( X is open iff for x being Element of REAL m st x in X holds
ex r being Real st
( r > 0 & { y where y is Element of REAL m : |.(y - x).| < r } c= X ) )