let a, b, r be Real; :: thesis: Ball (|[a,b]|,r) = inside_of_circle (a,b,r)
reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8;
thus Ball (|[a,b]|,r) = Ball (e,r) by Th11
.= inside_of_circle (a,b,r) by Th46 ; :: thesis: verum