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