let X be RealUnitarySpace; :: thesis: for x, y, 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 x, y, 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

dist (x,z) < r by A2, Th41;

then A3: r + (dist (x,z)) < r + r by XREAL_1:6;

A4: dist (y,z) <= (dist (y,x)) + (dist (x,z)) by BHSP_1:35;

dist (x,y) < r by A1, Th41;

then (dist (x,y)) + (dist (x,z)) < r + (dist (x,z)) by XREAL_1:6;

then (dist (x,y)) + (dist (x,z)) < 2 * r by A3, XXREAL_0:2;

hence dist (y,z) < 2 * r by A4, XXREAL_0:2; :: thesis: verum

for r being Real st y in Ball (x,r) & z in Ball (x,r) holds

dist (y,z) < 2 * r

let x, y, 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

dist (x,z) < r by A2, Th41;

then A3: r + (dist (x,z)) < r + r by XREAL_1:6;

A4: dist (y,z) <= (dist (y,x)) + (dist (x,z)) by BHSP_1:35;

dist (x,y) < r by A1, Th41;

then (dist (x,y)) + (dist (x,z)) < r + (dist (x,z)) by XREAL_1:6;

then (dist (x,y)) + (dist (x,z)) < 2 * r by A3, XXREAL_0:2;

hence dist (y,z) < 2 * r by A4, XXREAL_0:2; :: thesis: verum