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