:: deftheorem defines RotateCircle BORSUK_7:def 4 :
for r being non negative Real
for s being Real holds RotateCircle (r,s) = (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r));