let a be Real; :: thesis: for X being non empty compact Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p = 0. (TOP-REAL 2) & a > 0 holds
X c= Ball p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)
let X be non empty compact Subset of (TOP-REAL 2); :: thesis: for p being Point of (Euclid 2) st p = 0. (TOP-REAL 2) & a > 0 holds
X c= Ball p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)
let p be Point of (Euclid 2); :: thesis: ( p = 0. (TOP-REAL 2) & a > 0 implies X c= Ball p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a) )
assume that
A1: p = 0. (TOP-REAL 2) and
A2: a > 0 ; :: thesis: X c= Ball p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Ball p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a) )
assume A3: x in X ; :: thesis: x in Ball p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a)
then reconsider b = x as Point of (Euclid 2) by TOPREAL3:13;
set A = X;
set n = N-bound X;
set s = S-bound X;
set e = E-bound X;
set w = W-bound X;
set r = ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a;
reconsider P = p, B = b as Point of (TOP-REAL 2) by TOPREAL3:13;
A4: ( W-bound X <= B `1 & B `1 <= E-bound X & S-bound X <= B `2 & B `2 <= N-bound X ) by A3, PSCOMP_1:71;
A5: ( P `1 = 0 & P `2 = 0 ) by A1, Th32;
A6: dist p,b = (Pitag_dist 2) . p,b by METRIC_1:def 1
.= sqrt ((((P `1 ) - (B `1 )) ^2 ) + (((P `2 ) - (B `2 )) ^2 )) by TOPREAL3:12
.= sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 )) by A5 ;
( 0 <= (B `1 ) ^2 & 0 <= (B `2 ) ^2 ) by XREAL_1:65;
then sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 )) <= (sqrt ((B `1 ) ^2 )) + (sqrt ((B `2 ) ^2 )) by Th6;
then sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 )) <= (abs (B `1 )) + (sqrt ((B `2 ) ^2 )) by COMPLEX1:158;
then A7: sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 )) <= (abs (B `1 )) + (abs (B `2 )) by COMPLEX1:158;
A8: 0 <= abs (S-bound X) by COMPLEX1:132;
A9: 0 <= abs (W-bound X) by COMPLEX1:132;
A10: 0 <= abs (E-bound X) by COMPLEX1:132;
A11: 0 <= abs (N-bound X) by COMPLEX1:132;
A12: ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + 0 < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A2, XREAL_1:10;

now

per cases ( ( B `1 >= 0 & B `2 >= 0 ) or ( B `1 < 0 & B `2 >= 0 ) or ( B `1 >= 0 & B `2 < 0 ) or ( B `1 < 0 & B `2 < 0 ) ) ;

case ( B `1 >= 0 & B `2 >= 0 ) ; :: thesis: dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a

then ( abs (B `1 ) <= abs (E-bound X) & abs (B `2 ) <= abs (N-bound X) ) by A4, Th7;
then (abs (B `1 )) + (abs (B `2 )) <= (abs (E-bound X)) + (abs (N-bound X)) by XREAL_1:9;
then A13: dist p,b <= (abs (E-bound X)) + (abs (N-bound X)) by A6, A7, XXREAL_0:2;
((abs (E-bound X)) + (abs (N-bound X))) + 0 <= ((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X)) by A9, XREAL_1:9;
then (abs (E-bound X)) + (abs (N-bound X)) <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X)) by A8, XREAL_1:9;
then (abs (E-bound X)) + (abs (N-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A12, XXREAL_0:2;
hence dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A13, XXREAL_0:2; :: thesis: verum

end;

case ( B `1 < 0 & B `2 >= 0 ) ; :: thesis: dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a

then ( abs (B `1 ) <= abs (W-bound X) & abs (B `2 ) <= abs (N-bound X) ) by A4, Th7, Th8;
then (abs (B `1 )) + (abs (B `2 )) <= (abs (W-bound X)) + (abs (N-bound X)) by XREAL_1:9;
then A14: dist p,b <= (abs (W-bound X)) + (abs (N-bound X)) by A6, A7, XXREAL_0:2;
0 + ((abs (N-bound X)) + (abs (W-bound X))) <= (abs (E-bound X)) + ((abs (N-bound X)) + (abs (W-bound X))) by A10, XREAL_1:9;
then (abs (W-bound X)) + (abs (N-bound X)) <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X)) by A8, XREAL_1:9;
then (abs (W-bound X)) + (abs (N-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A12, XXREAL_0:2;
hence dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A14, XXREAL_0:2; :: thesis: verum

end;

case ( B `1 >= 0 & B `2 < 0 ) ; :: thesis: dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a

then ( abs (B `1 ) <= abs (E-bound X) & abs (B `2 ) <= abs (S-bound X) ) by A4, Th7, Th8;
then (abs (B `1 )) + (abs (B `2 )) <= (abs (E-bound X)) + (abs (S-bound X)) by XREAL_1:9;
then A15: dist p,b <= (abs (E-bound X)) + (abs (S-bound X)) by A6, A7, XXREAL_0:2;
A16: ((abs (E-bound X)) + (abs (S-bound X))) + 0 <= ((abs (E-bound X)) + (abs (S-bound X))) + (abs (N-bound X)) by A11, XREAL_1:9;
(((abs (E-bound X)) + (abs (N-bound X))) + (abs (S-bound X))) + 0 <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (S-bound X))) + (abs (W-bound X)) by A9, XREAL_1:9;
then (abs (E-bound X)) + (abs (S-bound X)) <= (((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X)) by A16, XXREAL_0:2;
then (abs (E-bound X)) + (abs (S-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A12, XXREAL_0:2;
hence dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A15, XXREAL_0:2; :: thesis: verum

end;

case ( B `1 < 0 & B `2 < 0 ) ; :: thesis: dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a

then ( abs (B `1 ) <= abs (W-bound X) & abs (B `2 ) <= abs (S-bound X) ) by A4, Th8;
then (abs (B `1 )) + (abs (B `2 )) <= (abs (W-bound X)) + (abs (S-bound X)) by XREAL_1:9;
then A17: dist p,b <= (abs (W-bound X)) + (abs (S-bound X)) by A6, A7, XXREAL_0:2;
0 + 0 <= (abs (E-bound X)) + (abs (N-bound X)) by A10, A11;
then 0 + ((abs (W-bound X)) + (abs (S-bound X))) <= ((abs (E-bound X)) + (abs (N-bound X))) + ((abs (W-bound X)) + (abs (S-bound X))) by XREAL_1:9;
then (abs (W-bound X)) + (abs (S-bound X)) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A2, XREAL_1:10;
hence dist p,b < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A17, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence x in Ball p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a) by METRIC_1:12; :: thesis: verum