let M be symmetric triangle MetrStruct ; :: thesis: for r being Real
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; :: 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:11;
A4: dist (x,q) < r by A2, METRIC_1:11;
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:8;
hence dist (p,q) < 2 * r by A5, XXREAL_0:2; :: thesis: verum