A1: PI / 2 < PI / 1 by XREAL_1:76;
A2: PI / 2 in ].0,PI.[ by A1, XXREAL_1:4;
then cot . (PI / 2) = 0 / (sin . (PI / 2)) by Th2, RFUNCT_1:def 1, SIN_COS:76
.= 0 ;
hence ( cot . (PI / 2) = 0 & cot (PI / 2) = 0 ) by A2, Th14; :: thesis: verum