for r being non negative Real
for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)