defpred S₁[ Element of X] means ||.(x - X).|| <= r;
set K = { q where q is Point of X : S₁[q] } ;
{ q where q is Point of X : S₁[q] } c= the carrier of X from FRAENKEL:sch 10();
then reconsider K = { q where q is Point of X : S₁[q] } as Subset of X ;
reconsider T = K as Subset of (TopSpaceNorm X) ;
T is closed by NORMSP_2:9;
hence cl_Ball (x,r) is closed by NORMSP_2:15; :: thesis: verum