let r, s, r1, r2 be Real; for u being Point of (Euclid 2) st u = |[r,s]| & 0 <= r2 & r2 < r1 holds
|[(r + r2),s]| in Ball (u,r1)
let u be Point of (Euclid 2); ( u = |[r,s]| & 0 <= r2 & r2 < r1 implies |[(r + r2),s]| in Ball (u,r1) )
assume that
A1:
u = |[r,s]|
and
A2:
0 <= r2
and
A3:
r2 < r1
; |[(r + r2),s]| in Ball (u,r1)
reconsider v = |[(r + r2),s]| as Point of (Euclid 2) by TOPREAL3:8;
dist (u,v) =
sqrt (((r - (r + r2)) ^2) + ((s - s) ^2))
by A1, Th6
.=
sqrt ((- (r - (r + r2))) ^2)
.=
r2
by A2, SQUARE_1:22
;
hence
|[(r + r2),s]| in Ball (u,r1)
by A3, METRIC_1:11; verum