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_{1} being Subset of M st b_{1} is empty )_{1} being Subset of M st b_{1} is empty

take X ; :: thesis: X is empty

thus X is empty ; :: thesis: verum

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

proof

assume
M is empty
; :: thesis: ex b
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_{1}[ Element of M9] means dist (p9,$1) <= r;

set X = { q where q is Element of M9 : S_{1}[q] } ;

{ q where q is Element of M9 : S_{1}[q] } c= the carrier of M9
from FRAENKEL:sch 10();

then reconsider X = { q where q is Element of M9 : S_{1}[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;then reconsider M9 = M as non empty MetrStruct ;

reconsider p9 = p as Element of M9 ;

defpred S

set X = { q where q is Element of M9 : S

{ q where q is Element of M9 : S

then reconsider X = { q where q is Element of M9 : S

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

take X ; :: thesis: X is empty

thus X is empty ; :: thesis: verum