let r be Real; 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 ; 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; ( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) )
assume
not M is empty
; ( 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
; 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; verum