PI / 4 < PI / 1 by XREAL_1:76;
then A1: PI / 4 < PI + ((2 * PI) * 0) ;
0 / 4 < PI / 4 by XREAL_1:74;
hence sin (PI / 4) > 0 by A1, SIN_COS6:11; :: thesis: verum