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