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 A4: PI / 2 in ].0 ,PI .[ by A2, XXREAL_1:4;
cot . (PI / 2) = 0 / (sin . (PI / 2)) by A4, Th2, RFUNCT_1:def 4, SIN_COS:81
.= 0 ;
hence ( cot . (PI / 2) = 0 & cot (PI / 2) = 0 ) by A4, Th14; :: thesis: verum