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:17;
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:13;
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:12
.= sqrt ((((x `1 ) - ((x `1 ) - (2 * a))) ^2 ) + (((x `2 ) - (|[((x `1 ) - (2 * a)),(x `2 )]| `2 )) ^2 )) by EUCLID:56
.= sqrt ((((0 ^2 ) + ((2 * ((x `1 ) - (x `1 ))) * (2 * a))) + ((2 * a) ^2 )) + (((x `2 ) - (x `2 )) ^2 )) by EUCLID:56
.= 2 * a by A2, SQUARE_1:89 ;
assume |[((x `1 ) - (2 * a)),(x `2 )]| in Ball f,a ; :: thesis: contradiction
then A4: dist f,z < a by METRIC_1:12;
dist f,X < a by A1, METRIC_1:12;
then (dist f,X) + (dist f,z) < a + a by A4, XREAL_1:10;
hence contradiction by A3, METRIC_1:4; :: thesis: verum