theorem :: SIN_COS9:58

for r being Real st - 1 <= r & r <= 1 & arccot r = (3 / 4) * PI holds
r = - 1 by Th18, Th52;