reconsider X = {} as Subset of M by XBOOLE_1:2;
thus ( not M is empty implies ex X being Subset of M st X = { q where q is Element of M : dist (p,q) = r } ) :: thesis:

assume not M is empty ; :: thesis:
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
defpred S₁[ Element of M9] means dist (p9,$1) = r;
set X = { q where q is Element of M9 : S₁[q] } ;
{ q where q is Element of M9 : S₁[q] } c= the carrier of M9 from FRAENKEL:sch 10();
then reconsider X = { q where q is Element of M9 : S₁[q] } as Subset of M ;
take X ; :: thesis:
thus X = { q where q is Element of M : dist (p,q) = r } ; :: thesis:

end;