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

proof

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

end;

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