PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: PI > 0 by XXREAL_1:4;
then A2: PI / 2 > 0 / 2 by XREAL_1:76;
PI / 2 < PI / 1 by A1, XREAL_1:78;
then arccot 0 = PI / 2 by A2, Th34, Th40;
hence ( arccot 0 = PI / 2 & arccot . 0 = PI / 2 ) ; :: thesis: verum