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