A1: (3 / 4) * PI < PI by Lm10, XXREAL_1:4;
arccot (- 1) = (3 / 4) * PI by A1, Th18, Th36;
hence ( arccot (- 1) = (3 / 4) * PI & arccot . (- 1) = (3 / 4) * PI ) ; :: thesis: verum