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