let a, b, r be real number ; :: thesis: cl_Ball |[a,b]|,r = closed_inside_of_circle a,b,r
reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:13;
thus cl_Ball |[a,b]|,r = cl_Ball e,r by Th14
.= closed_inside_of_circle a,b,r by Th47 ; :: thesis: verum