:: deftheorem defines Sphere TOPREAL9:def 3 :
for n being Nat
for x being Point of (TOP-REAL n)
for r being Real holds Sphere (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ;