let X be RealUnitarySpace; :: thesis: for x, y, z being Point of X

for r being Real st y in Ball (x,r) holds

y - z in Ball ((x - z),r)

let x, y, z be Point of X; :: thesis: for r being Real st y in Ball (x,r) holds

y - z in Ball ((x - z),r)

let r be Real; :: thesis: ( y in Ball (x,r) implies y - z in Ball ((x - z),r) )

assume y in Ball (x,r) ; :: thesis: y - z in Ball ((x - z),r)

then A1: dist (x,y) < r by Th41;

dist ((x - z),(y - z)) = dist (x,y) by BHSP_1:42;

hence y - z in Ball ((x - z),r) by A1, Th41; :: thesis: verum

for r being Real st y in Ball (x,r) holds

y - z in Ball ((x - z),r)

let x, y, z be Point of X; :: thesis: for r being Real st y in Ball (x,r) holds

y - z in Ball ((x - z),r)

let r be Real; :: thesis: ( y in Ball (x,r) implies y - z in Ball ((x - z),r) )

assume y in Ball (x,r) ; :: thesis: y - z in Ball ((x - z),r)

then A1: dist (x,y) < r by Th41;

dist ((x - z),(y - z)) = dist (x,y) by BHSP_1:42;

hence y - z in Ball ((x - z),r) by A1, Th41; :: thesis: verum