theorem Th36: :: SIN_COS9:36

for r being Real st 0 < r & r < PI holds
( arccot (cot . r) = r & arccot (cot r) = r )