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:13;
reconsider e = u as Point of (Euclid 2) by TOPREAL3:13;
dist e,x = |.(u - |[a,b]|).| by A1, JGRAPH_1:45;
then |.(u - |[a,b]|).| < r by A2, METRIC_1:12;
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:13;
dist e,x = |.(u - |[a,b]|).| by A1, JGRAPH_1:45;
then dist e,x < r by A3, Th45;
hence w in Ball x,r by METRIC_1:12; :: thesis: verum