let r, s, s1, s2 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:8;
dist (u,v) = sqrt (((r - r) ^2) + ((s - (s + s2)) ^2)) by A1, Th6
.= sqrt ((- (s - (s + s2))) ^2)
.= s2 by A2, SQUARE_1:22 ;
hence |[r,(s + s2)]| in Ball (u,s1) by A3, METRIC_1:11; :: thesis: verum