let r, s, s2, s1 be Real; :: thesis: for u being Point of (Euclid 2) st u = |[r,s]| & 0 <= s2 & s2 < s1 holds
|[r,(s + s2)]| in Ball u,s1
let u be Point of (Euclid 2); :: thesis: ( u = |[r,s]| & 0 <= s2 & s2 < s1 implies |[r,(s + s2)]| in Ball u,s1 )
assume that
A1: u = |[r,s]| and
A2: 0 <= s2 and
A3: s2 < s1 ; :: thesis: |[r,(s + s2)]| in Ball u,s1
reconsider v = |[r,(s + s2)]| as Point of (Euclid 2) by TOPREAL3:13;
dist u,v = sqrt (((r - r) ^2 ) + ((s - (s + s2)) ^2 )) by A1, Th9
.= sqrt ((- (s - (s + s2))) ^2 )
.= s2 by A2, SQUARE_1:89 ;
hence |[r,(s + s2)]| in Ball u,s1 by A3, METRIC_1:12; :: thesis: verum