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))
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;
A3: ((((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:8;
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 A4: 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:8;
reconsider P = p, B = b as Point of (TOP-REAL 2) by TOPREAL3:8;
A5: P `1 = 0 by A1, Th32;
A6: B `1 <= E-bound X by A4, PSCOMP_1:24;
A7: B `2 <= N-bound X by A4, PSCOMP_1:24;
A8: S-bound X <= B `2 by A4, PSCOMP_1:24;
A9: P `2 = 0 by A1, Th32;
A10: 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:7
.= sqrt (((B `1) ^2) + ((B `2) ^2)) by A5, A9 ;
A11: 0 <= (B `2) ^2 by XREAL_1:63;
0 <= (B `1) ^2 by XREAL_1:63;
then sqrt (((B `1) ^2) + ((B `2) ^2)) <= (sqrt ((B `1) ^2)) + (sqrt ((B `2) ^2)) by A11, Th6;
then sqrt (((B `1) ^2) + ((B `2) ^2)) <= (abs (B `1)) + (sqrt ((B `2) ^2)) by COMPLEX1:72;
then A12: sqrt (((B `1) ^2) + ((B `2) ^2)) <= (abs (B `1)) + (abs (B `2)) by COMPLEX1:72;
A13: 0 <= abs (N-bound X) by COMPLEX1:46;
A14: 0 <= abs (E-bound X) by COMPLEX1:46;
A15: 0 <= abs (W-bound X) by COMPLEX1:46;
A16: 0 <= abs (S-bound X) by COMPLEX1:46;
A17: W-bound X <= B `1 by A4, PSCOMP_1:24;

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 A18: ( 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

((abs (E-bound X)) + (abs (N-bound X))) + 0 <= ((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X)) by A15, XREAL_1:7;
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 A16, XREAL_1:7;
then A19: (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 A3, XXREAL_0:2;
A20: abs (B `2) <= abs (N-bound X) by A7, A18, Th7;
abs (B `1) <= abs (E-bound X) by A6, A18, Th7;
then (abs (B `1)) + (abs (B `2)) <= (abs (E-bound X)) + (abs (N-bound X)) by A20, XREAL_1:7;
then dist (p,b) <= (abs (E-bound X)) + (abs (N-bound X)) by A10, 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 A19, XXREAL_0:2; :: thesis: verum

end;

case A21: ( 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

0 + ((abs (N-bound X)) + (abs (W-bound X))) <= (abs (E-bound X)) + ((abs (N-bound X)) + (abs (W-bound X))) by A14, XREAL_1:7;
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 A16, XREAL_1:7;
then A22: (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 A3, XXREAL_0:2;
A23: abs (B `2) <= abs (N-bound X) by A7, A21, Th7;
abs (B `1) <= abs (W-bound X) by A17, A21, Th8;
then (abs (B `1)) + (abs (B `2)) <= (abs (W-bound X)) + (abs (N-bound X)) by A23, XREAL_1:7;
then dist (p,b) <= (abs (W-bound X)) + (abs (N-bound X)) by A10, 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 A22, XXREAL_0:2; :: thesis: verum

end;

case A24: ( 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

A25: (((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 A15, XREAL_1:7;
((abs (E-bound X)) + (abs (S-bound X))) + 0 <= ((abs (E-bound X)) + (abs (S-bound X))) + (abs (N-bound X)) by A13, XREAL_1:7;
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 A25, XXREAL_0:2;
then A26: (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 A3, XXREAL_0:2;
A27: abs (B `2) <= abs (S-bound X) by A8, A24, Th8;
abs (B `1) <= abs (E-bound X) by A6, A24, Th7;
then (abs (B `1)) + (abs (B `2)) <= (abs (E-bound X)) + (abs (S-bound X)) by A27, XREAL_1:7;
then dist (p,b) <= (abs (E-bound X)) + (abs (S-bound X)) by A10, 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 A26, XXREAL_0:2; :: thesis: verum

end;

case A28: ( 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 A29: abs (B `2) <= abs (S-bound X) by A8, Th8;
abs (B `1) <= abs (W-bound X) by A17, A28, Th8;
then (abs (B `1)) + (abs (B `2)) <= (abs (W-bound X)) + (abs (S-bound X)) by A29, XREAL_1:7;
then A30: dist (p,b) <= (abs (W-bound X)) + (abs (S-bound X)) by A10, A12, XXREAL_0:2;
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 A14, A13, XREAL_1:7;
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:8;
hence dist (p,b) < ((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a by A30, 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:11; :: thesis: verum