let a, b, r be real number ; :: thesis: Ball |[a,b]|,r = inside_of_circle a,b,r
reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:13;
thus Ball |[a,b]|,r = Ball e,r by Th13
.= inside_of_circle a,b,r by Th48 ; :: thesis: verum