let a be Real; for f being Point of (Euclid 2)
for x being Point of (TOP-REAL 2) st x in Ball (f,a) holds
not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a)
let f be Point of (Euclid 2); for x being Point of (TOP-REAL 2) st x in Ball (f,a) holds
not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a)
let x be Point of (TOP-REAL 2); ( x in Ball (f,a) implies not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a) )
assume A1:
x in Ball (f,a)
; not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a)
A2:
a > 0
by A1, TBSP_1:12;
set p = |[((x `1) - (2 * a)),(x `2)]|;
reconsider z = |[((x `1) - (2 * a)),(x `2)]|, X = x as Point of (Euclid 2) by TOPREAL3:8;
A3: dist (X,z) =
(Pitag_dist 2) . (X,z)
by METRIC_1:def 1
.=
sqrt ((((x `1) - (|[((x `1) - (2 * a)),(x `2)]| `1)) ^2) + (((x `2) - (|[((x `1) - (2 * a)),(x `2)]| `2)) ^2))
by TOPREAL3:7
.=
sqrt ((((x `1) - ((x `1) - (2 * a))) ^2) + (((x `2) - (|[((x `1) - (2 * a)),(x `2)]| `2)) ^2))
by EUCLID:52
.=
sqrt ((((0 ^2) + ((2 * ((x `1) - (x `1))) * (2 * a))) + ((2 * a) ^2)) + (((x `2) - (x `2)) ^2))
by EUCLID:52
.=
2 * a
by A2, SQUARE_1:22
;
assume
|[((x `1) - (2 * a)),(x `2)]| in Ball (f,a)
; contradiction
then A4:
dist (f,z) < a
by METRIC_1:11;
dist (f,X) < a
by A1, METRIC_1:11;
then
(dist (f,X)) + (dist (f,z)) < a + a
by A4, XREAL_1:8;
hence
contradiction
by A3, METRIC_1:4; verum