for V being RealUnitarySpace
for M being Subset of (TopUnitSpace V) holds
( M is open iff for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball (v,r) c= M ) ) by Def5;