defpred S₁[ Element of COMPLEX n] means dist ($1,A) < 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 : dist (z,A) < r } is Subset of (COMPLEX n) ; :: thesis: verum