for r, s being Real
for p being Point of (TOP-REAL 2) holds
( p in Sphere ((0. (TOP-REAL 2)),r) iff (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) )