let a, b, r be Real; :: 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 object ; :: 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: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:12;
hence w in closed_inside_of_circle (a,b,r) by Th42; :: thesis: verum

end;

let w be object ; :: 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:8;
dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28;
then dist (e,x) <= r by A3, Th42;
hence w in cl_Ball (x,r) by METRIC_1:12; :: thesis: verum