let r, s, r1, r2 be Real; :: thesis: 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); :: thesis: ( 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 ; :: thesis: |[(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; :: thesis: verum