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:13;
thus Sphere |[a,b]|,r = Sphere e,r by Th15
.= circle a,b,r by Th49 ; :: thesis: verum