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