let X be RealUnitarySpace; :: thesis: for y, x, z being Point of X
for r being Real st y in Ball x,r & z in Ball x,r holds
dist y,z < 2 * r
let y, x, z be Point of X; :: thesis: for r being Real st y in Ball x,r & z in Ball x,r holds
dist y,z < 2 * r
let r be Real; :: thesis: ( y in Ball x,r & z in Ball x,r implies dist y,z < 2 * r )
assume that
A1: y in Ball x,r and
A2: z in Ball x,r ; :: thesis: dist y,z < 2 * r
A3: dist x,y < r by A1, Th41;
A4: dist x,z < r by A2, Th41;
A5: (dist x,y) + (dist x,z) < r + (dist x,z) by A3, XREAL_1:8;
r + (dist x,z) < r + r by A4, XREAL_1:8;
then A6: (dist x,y) + (dist x,z) < 2 * r by A5, XXREAL_0:2;
dist y,z <= (dist y,x) + (dist x,z) by BHSP_1:42;
hence dist y,z < 2 * r by A6, XXREAL_0:2; :: thesis: verum