let a, b, r be Real; :: thesis: cl_Ball (|[a,b]|,r) = closed_inside_of_circle (a,b,r)
reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8;
thus cl_Ball (|[a,b]|,r) = cl_Ball (e,r) by Th12
.= closed_inside_of_circle (a,b,r) by Th45 ; :: thesis: verum