let x be Real; :: thesis: ( x in ].(PI / 2),((3 / 2) * PI).[ implies cos . x < 0 )
A1: sin . (x + (PI / 2)) = cos . x by SIN_COS:78;
assume A2: x in ].(PI / 2),((3 / 2) * PI).[ ; :: thesis: cos . x < 0
then x < (3 / 2) * PI by XXREAL_1:4;
then A3: x + (PI / 2) < ((3 / 2) * PI) + (PI / 2) by XREAL_1:6;
PI / 2 < x by A2, XXREAL_1:4;
then (PI / 2) + (PI / 2) < x + (PI / 2) by XREAL_1:6;
then x + (PI / 2) in ].PI,(2 * PI).[ by A3, XXREAL_1:4;
hence cos . x < 0 by A1, Th9; :: thesis: verum