:: deftheorem Def5 defines Family_open_set RUSUB_5:def 5 :
for V being RealUnitarySpace
for b₂ being Subset-Family of V holds
( b₂ = Family_open_set V iff for M being Subset of V holds
( M in b₂ iff for x being Point of V st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) ) );