defpred S_{1}[ Point of X] means ||.(x - $1).|| < r;

{ y where y is Point of X : S_{1}[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

{ y where y is Point of X : S

hence { y where y is Point of X : ||.(x - y).|| < r } is Subset of X ; :: thesis: verum