theorem :: SIN_COS9:34

arccot * (cot | ].0,PI.[) = id ].0,PI.[ by Lm6, Th12, FUNCT_1:39;