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