let a be Real; :: thesis: 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); :: thesis: 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); :: thesis: ( x in Ball (f,a) implies not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a) )
assume A1: x in Ball (f,a) ; :: thesis: 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))
.= sqrt ((((0 ^2) + ((2 * ((x `1) - (x `1))) * (2 * a))) + ((2 * a) ^2)) + (((x `2) - (x `2)) ^2))
.= 2 * a by A2, SQUARE_1:22 ;
assume |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a) ; :: thesis: 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; :: thesis: verum