A1: PI / 4 < PI by Lm9, XXREAL_1:4;
0 < PI / 4 by Lm9, XXREAL_1:4;
then arccot 1 = PI / 4 by A1, Th18, Th36;
hence ( arccot 1 = PI / 4 & arccot . 1 = PI / 4 ) ; :: thesis: verum