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