let r be Real; :: thesis: for M being MetrStruct

for p, x being Element of M holds

( x in Sphere (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 Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )

let p, x be Element of M; :: thesis: ( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )

then reconsider M9 = M as non empty MetrStruct ;

reconsider p9 = p as Element of M9 ;

assume dist (p,x) = r ; :: thesis: x in Sphere (p,r)

then x in { q where q is Element of M9 : dist (p9,q) = r } ;

hence x in Sphere (p,r) by Def16; :: thesis: verum

for p, x being Element of M holds

( x in Sphere (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 Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )

let p, x be Element of M; :: thesis: ( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )

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

assume
not M is empty
; :: thesis: ( not dist (p,x) = r or x in Sphere (p,r) )assume A1:
x in Sphere (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, Def16;

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;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, Def16;

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

then reconsider M9 = M as non empty MetrStruct ;

reconsider p9 = p as Element of M9 ;

assume dist (p,x) = r ; :: thesis: x in Sphere (p,r)

then x in { q where q is Element of M9 : dist (p9,q) = r } ;

hence x in Sphere (p,r) by Def16; :: thesis: verum