thus ( not M is empty implies ex X being Subset of M ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & 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 ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & X = { q where q is Element of M' : dist p',q <= r } )
then reconsider M' = M as non empty MetrStruct ;
reconsider p' = p as Element of M' ;
defpred S₁[ Element of M'] means dist p',$1 <= r;
set X = { q where q is Element of M' : S₁[q] } ;
{ q where q is Element of M' : S₁[q] } c= the carrier of M' from FRAENKEL:sch 10();
then reconsider X = { q where q is Element of M' : S₁[q] } as Subset of M ;
take X ; :: thesis: ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & X = { q where q is Element of M' : dist p',q <= r } )
take M' ; :: thesis: ex p' being Element of M' st
( M' = M & p' = p & X = { q where q is Element of M' : dist p',q <= r } )
take p' ; :: thesis: ( M' = M & p' = p & X = { q where q is Element of M' : dist p',q <= r } )
thus ( M' = M & p' = p & 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
reconsider X = {} as Subset of M by XBOOLE_1:2;
take X ; :: thesis: X is empty
thus X is empty ; :: thesis: verum