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