let M be symmetric triangle MetrStruct ; 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; 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; ( 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)
; 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; verum