PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: ( 0 < PI & PI < 4 ) by XXREAL_1:4;
0 / 2 < PI / 2 by A1, XREAL_1:76;
then (PI / 2) * (- 1) < 0 * (- 1) by XREAL_1:71;
then ( (- (PI / 2)) + ((2 * PI ) * 0 ) < PI / 4 & PI / 4 < (PI / 2) + ((2 * PI ) * 0 ) ) by A1, XREAL_1:78;
hence cos (PI / 4) > 0 by SIN_COS6:13; :: thesis: verum