let X be ComplexUnitarySpace; :: thesis: for y, x, w being Point of X
for r being Real st y in Ball x,r holds
y - w in Ball (x - w),r
let y, x, w be Point of X; :: thesis: for r being Real st y in Ball x,r holds
y - w in Ball (x - w),r
let r be Real; :: thesis: ( y in Ball x,r implies y - w in Ball (x - w),r )
assume y in Ball x,r ; :: thesis: y - w in Ball (x - w),r
then A1: dist x,y < r by Th41;
dist (x - w),(y - w) = dist x,y by CSSPACE:61;
hence y - w in Ball (x - w),r by A1, Th41; :: thesis: verum