defpred S₁[ Element of M] means ||.(p - $1).|| <= r;
set X = { q where q is Element of M : S₁[q] } ;
{ q where q is Element of M : S₁[q] } c= the carrier of M from FRAENKEL:sch 10();
hence { q where q is Element of M : ||.(p - q).|| <= r } is Subset of M ; :: thesis: verum