let a, b, r be real number ; :: 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 Th15
.= circle (a,b,r) by Th49 ; :: thesis: verum