let n be Nat; :: thesis: for a, b being Real
for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b
let a, b be Real; :: thesis: for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b
let x, y be Point of (Euclid n); :: thesis: ( Ball (x,a) meets Ball (y,b) implies dist (x,y) < a + b )
assume Ball (x,a) meets Ball (y,b) ; :: thesis: dist (x,y) < a + b
then consider z being object such that
A1: z in Ball (x,a) and
A2: z in Ball (y,b) by XBOOLE_0:3;
reconsider z = z as Point of (Euclid n) by A1;
dist (y,z) < b by A2, METRIC_1:11;
then A3: (dist (x,z)) + (dist (y,z)) < (dist (x,z)) + b by XREAL_1:8;
A4: (dist (x,z)) + (dist (y,z)) >= dist (x,y) by METRIC_1:4;
dist (x,z) < a by A1, METRIC_1:11;
then (dist (x,z)) + b < a + b by XREAL_1:8;
then (dist (x,z)) + (dist (y,z)) < a + b by A3, XXREAL_0:2;
hence dist (x,y) < a + b by A4, XXREAL_0:2; :: thesis: verum