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 open by NORMSP_2:8;
hence Ball (x,r) is open by NORMSP_2:16; :: thesis: verum