let X be RealUnitarySpace; :: thesis: for y, x, z being Point of X
for r being Real st y in Ball x,r holds
y - z in Ball (x - z),r
let y, x, 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:49;
hence y - z in Ball (x - z),r by A1, Th41; :: thesis: verum