let a, b, r be real number ; :: thesis: for x being Point of (Euclid 2) st x = |[a,b]| holds
Ball (x,r) = inside_of_circle (a,b,r)
let x be Point of (Euclid 2); :: thesis: ( x = |[a,b]| implies Ball (x,r) = inside_of_circle (a,b,r) )
assume A1: x = |[a,b]| ; :: thesis: Ball (x,r) = inside_of_circle (a,b,r)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: inside_of_circle (a,b,r) c= Ball (x,r)

let w be set ; :: thesis: ( w in Ball (x,r) implies w in inside_of_circle (a,b,r) )
assume A2: w in Ball (x,r) ; :: thesis: w in inside_of_circle (a,b,r)
then reconsider u = w as Point of (TOP-REAL 2) by TOPREAL3:8;
reconsider e = u as Point of (Euclid 2) by TOPREAL3:8;
dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28;
then |.(u - |[a,b]|).| < r by A2, METRIC_1:11;
hence w in inside_of_circle (a,b,r) by Th45; :: thesis: verum

end;

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in inside_of_circle (a,b,r) or w in Ball (x,r) )
assume A3: w in inside_of_circle (a,b,r) ; :: thesis: w in Ball (x,r)
then reconsider u = w as Point of (TOP-REAL 2) ;
reconsider e = u as Point of (Euclid 2) by TOPREAL3:8;
dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28;
then dist (e,x) < r by A3, Th45;
hence w in Ball (x,r) by METRIC_1:11; :: thesis: verum