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

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