let a, b, r be Real; :: thesis: Sphere (|[a,b]|,r) = circle (a,b,r)
reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8;
thus Sphere (|[a,b]|,r) = Sphere (e,r) by Th13
.= circle (a,b,r) by Th47 ; :: thesis: verum