let r be Real; :: 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 )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
x in { q where q is Element of M9 : dist (p9,q) <= r } by A1, Def15;
then ex q being Element of M st
( x = q & dist (p,q) <= r ) ;
hence ( not M is empty & dist (p,x) <= r ) by A1; :: thesis: verum
end;
assume not M is empty ; :: thesis: ( not dist (p,x) <= r or x in cl_Ball (p,r) )
then reconsider M9 = M as non empty MetrStruct ;
reconsider p9 = p as Element of M9 ;
assume dist (p,x) <= r ; :: thesis: x in cl_Ball (p,r)
then x in { q where q is Element of M9 : dist (p9,q) <= r } ;
hence x in cl_Ball (p,r) by Def15; :: thesis: verum