let V be RealUnitarySpace; :: thesis: for v being Point of V
for r being Real holds Ball v,r in Family_open_set V
let v be Point of V; :: thesis: for r being Real holds Ball v,r in Family_open_set V
let r be Real; :: thesis: Ball v,r in Family_open_set V
for u being Point of V st u in Ball v,r holds
ex p being Real st
( p > 0 & Ball u,p c= Ball v,r ) by Th35;
hence Ball v,r in Family_open_set V by Def5; :: thesis: verum