defpred S₁[ Subset of V] means for x being Point of V st x in $1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= $1 );
ex F being Subset-Family of V st
for M being Subset of V holds
( M in F iff S₁[M] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of V st
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 ) ) ; :: thesis: verum