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