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

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: closed_inside_of_circle a,b,r c= cl_Ball x,r

let w be set ; :: thesis: ( w in cl_Ball x,r implies w in closed_inside_of_circle a,b,r )
assume A2: w in cl_Ball x,r ; :: thesis: w in closed_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:13;
hence w in closed_inside_of_circle a,b,r by Th44; :: thesis: verum

end;

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in closed_inside_of_circle a,b,r or w in cl_Ball x,r )
assume A3: w in closed_inside_of_circle a,b,r ; :: thesis: w in cl_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, Th44;
hence w in cl_Ball x,r by METRIC_1:13; :: thesis: verum