theorem :: SIN_COS9:62

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