let M be symmetric triangle MetrStruct ; :: thesis: for r being real number
for p, q, x being Element of M st p in Ball x,r & q in Ball x,r holds
dist p,q < 2 * r
let r be real number ; :: thesis: for p, q, x being Element of M st p in Ball x,r & q in Ball x,r holds
dist p,q < 2 * r
let p, q, x be Element of M; :: thesis: ( p in Ball x,r & q in Ball x,r implies dist p,q < 2 * r )
assume that
A1: p in Ball x,r and
A2: q in Ball x,r ; :: thesis: dist p,q < 2 * r
A3: dist p,x < r by A1, METRIC_1:12;
A4: dist x,q < r by A2, METRIC_1:12;
A5: dist p,q <= (dist p,x) + (dist x,q) by METRIC_1:4;
(dist p,x) + (dist x,q) < r + r by A3, A4, XREAL_1:10;
hence dist p,q < 2 * r by A5, XXREAL_0:2; :: thesis: verum