let X be ComplexUnitarySpace; :: thesis: for x, y, w being Point of X
for r being Real st y in Ball (x,r) & w in Ball (x,r) holds
dist (y,w) < 2 * r
let x, y, w be Point of X; :: thesis: for r being Real st y in Ball (x,r) & w in Ball (x,r) holds
dist (y,w) < 2 * r
let r be Real; :: thesis: ( y in Ball (x,r) & w in Ball (x,r) implies dist (y,w) < 2 * r )
assume that
A1: y in Ball (x,r) and
A2: w in Ball (x,r) ; :: thesis: dist (y,w) < 2 * r
dist (x,w) < r by A2, Th41;
then A3: r + (dist (x,w)) < r + r by XREAL_1:6;
A4: dist (y,w) <= (dist (y,x)) + (dist (x,w)) by CSSPACE:51;
dist (x,y) < r by A1, Th41;
then (dist (x,y)) + (dist (x,w)) < r + (dist (x,w)) by XREAL_1:6;
then (dist (x,y)) + (dist (x,w)) < 2 * r by A3, XXREAL_0:2;
hence dist (y,w) < 2 * r by A4, XXREAL_0:2; :: thesis: verum