let r, s, r2, r1 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:13;
dist u,v = sqrt (((r - (r + r2)) ^2 ) + ((s - s) ^2 )) by A1, Th9
.= sqrt ((- (r - (r + r2))) ^2 )
.= r2 by A2, SQUARE_1:89 ;
hence |[(r + r2),s]| in Ball u,r1 by A3, METRIC_1:12; :: thesis: verum