let X be ComplexUnitarySpace; :: thesis: for y, x, 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 y, x, 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:8;
A4: dist y,w <= (dist y,x) + (dist x,w) by CSSPACE:54;
dist x,y < r by A1, Th41;
then (dist x,y) + (dist x,w) < r + (dist x,w) by XREAL_1:8;
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