let q, p be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for r being real number 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); :: thesis: for r being real number st e = q & p in Ball e,r holds
( (q `2 ) - r < p `2 & p `2 < (q `2 ) + r )
let r be real number ; :: thesis: ( 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 ; :: thesis: ( (q `2 ) - r < p `2 & p `2 < (q `2 ) + r )
reconsider f = p as Point of (Euclid 2) by TOPREAL3:13;
A3: dist e,f < r by A2, METRIC_1:12;
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:12 ;
A5: r > 0 by A2, TBSP_1:17;
then A6: r ^2 > 0 by SQUARE_1:74;
assume A7: ( not (q `2 ) - r < p `2 or not p `2 < (q `2 ) + r ) ; :: thesis: contradiction

per cases ( (q `2 ) - r >= p `2 or p `2 >= (q `2 ) + r ) by A7;

suppose (q `2 ) - r >= p `2 ; :: thesis: contradiction

then (q `2 ) - (p `2 ) >= r by XREAL_1:13;
then A8: ((q `2 ) - (p `2 )) ^2 >= r ^2 by A5, SQUARE_1:77;
((q `1 ) - (p `1 )) ^2 >= 0 by XREAL_1:65;
then (((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ) >= (((q `2 ) - (p `2 )) ^2 ) + 0 by XREAL_1:8;
then (((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ) >= r ^2 by A8, XXREAL_0:2;
then sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= sqrt (r ^2 ) by A6, SQUARE_1:94;
hence contradiction by A3, A4, A5, SQUARE_1:89; :: thesis: verum

end;

suppose p `2 >= (q `2 ) + r ; :: thesis: contradiction

then (p `2 ) - (q `2 ) >= r by XREAL_1:21;
then A9: (- ((q `2 ) - (p `2 ))) ^2 >= r ^2 by A5, SQUARE_1:77;
((q `1 ) - (p `1 )) ^2 >= 0 by XREAL_1:65;
then (((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ) >= (((q `2 ) - (p `2 )) ^2 ) + 0 by XREAL_1:8;
then (((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ) >= r ^2 by A9, XXREAL_0:2;
then sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= sqrt (r ^2 ) by A6, SQUARE_1:94;
hence contradiction by A3, A4, A5, SQUARE_1:89; :: thesis: verum

end;

end;