theorem Th64: :: SIN_COS9:64

for r being Real st - 1 <= r & r <= 1 holds
( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI )