PI in ].0,4.[ by SIN_COS:def 28;
then A1: 0 < PI by XXREAL_1:4;
then 0 / 4 < PI / 4 by XREAL_1:74;
then A2: (PI / 4) * (- 1) < 0 * (- 1) by XREAL_1:69;
PI / 4 < PI / 1 by A1, XREAL_1:76;
then A3: PI * (- 1) < (PI / 4) * (- 1) by XREAL_1:69;
for r being Real st PI + ((2 * PI) * (- 1)) < r & r < (2 * PI) + ((2 * PI) * (- 1)) holds
sin r < 0 by SIN_COS6:12;
hence sin (- (PI / 4)) < 0 by A2, A3; :: thesis: verum