defpred S₁[ set ] means for x being Element of PM st x in $1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= $1 );
thus ex S being Subset-Family of PM st
for V being Subset of PM holds
( V in S iff S₁[V] ) from SUBSET_1:sch 3(); :: thesis: verum