defpred S₁[ FinSequence of COMPLEX ] means |.($1 - x).| < r;
{ z where z is Element of COMPLEX n : S₁[z] } c= COMPLEX n from FRAENKEL:sch 10();
hence { z where z is Element of COMPLEX n : |.(z - x).| < r } is Subset of (COMPLEX n) ; :: thesis: verum