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 );
consider F being Subset-Family of V such that
A1: for M being Subset of V holds
( M in F iff S₁[M] ) from SUBSET_1:sch 3();
thus 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 ) ) by A1; :: thesis: verum