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