theorem Th50: :: SIN_COS9:50
for x being set st x in [.(- 1),1.] holds
arccot . x in [.(PI / 4),((3 / 4) * PI).]