( 0 < (3 / 4) * PI & (3 / 4) * PI < PI ) by Lm10, XXREAL_1:4;
then arccot (- 1) = (3 / 4) * PI by Th16, Th34;
hence ( arccot (- 1) = (3 / 4) * PI & arccot . (- 1) = (3 / 4) * PI ) ; :: thesis: verum