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: ( M is empty implies ex b₁ being Subset of M st b₁ is empty )

proof

assume not M is empty ; :: thesis: ex X being Subset of M st X = { q where q is Element of M : dist (p,q) <= r }
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: X = { q where q is Element of M : dist (p,q) <= r }
thus X = { q where q is Element of M : dist (p,q) <= r } ; :: thesis: verum

end;

assume M is empty ; :: thesis: ex b₁ being Subset of M st b₁ is empty
take X ; :: thesis: X is empty
thus X is empty ; :: thesis: verum