let p, q be Point of (TOP-REAL 2); for e being Point of (Euclid 2)
for r being Real st e = q & p in Ball (e,r) holds
( (q `2) - r < p `2 & p `2 < (q `2) + r )
let e be Point of (Euclid 2); for r being Real st e = q & p in Ball (e,r) holds
( (q `2) - r < p `2 & p `2 < (q `2) + r )
let r be Real; ( e = q & p in Ball (e,r) implies ( (q `2) - r < p `2 & p `2 < (q `2) + r ) )
assume that
A1:
e = q
and
A2:
p in Ball (e,r)
; ( (q `2) - r < p `2 & p `2 < (q `2) + r )
reconsider f = p as Point of (Euclid 2) by TOPREAL3:8;
A3:
dist (e,f) < r
by A2, METRIC_1:11;
A4: dist (e,f) =
(Pitag_dist 2) . (e,f)
by METRIC_1:def 1
.=
sqrt ((((q `1) - (p `1)) ^2) + (((q `2) - (p `2)) ^2))
by A1, TOPREAL3:7
;
A5:
r > 0
by A2, TBSP_1:12;
assume A6:
( not (q `2) - r < p `2 or not p `2 < (q `2) + r )
; contradiction