let r be real number ; :: thesis: for M being MetrStruct
for p, x being Element of M holds
( x in cl_Ball p,r iff ( not M is empty & dist p,x <= r ) )
let M be MetrStruct ; :: thesis: for p, x being Element of M holds
( x in cl_Ball p,r iff ( not M is empty & dist p,x <= r ) )
let p, x be Element of M; :: thesis: ( x in cl_Ball p,r iff ( not M is empty & dist p,x <= r ) )

hereby :: thesis: ( not M is empty & dist p,x <= r implies x in cl_Ball p,r )

assume A1: x in cl_Ball p,r ; :: thesis: ( not M is empty & dist p,x <= r )
A2: not M is empty by A1;
then reconsider M' = M as non empty MetrStruct ;
reconsider p' = p as Element of M' ;
x in { q where q is Element of M' : dist p',q <= r } by A1, Lm7;
then ex q being Element of M st
( x = q & dist p,q <= r ) ;
hence ( not M is empty & dist p,x <= r ) by A2; :: thesis: verum

end;

assume not M is empty ; :: thesis: ( not dist p,x <= r or x in cl_Ball p,r )
then reconsider M' = M as non empty MetrStruct ;
reconsider p' = p as Element of M' ;
assume dist p,x <= r ; :: thesis: x in cl_Ball p,r
then x in { q where q is Element of M' : dist p',q <= r } ;
hence x in cl_Ball p,r by Lm7; :: thesis: verum