let x be real number ; :: thesis: ( x in ].(PI / 2),((3 / 2) * PI ).[ implies cos . x < 0 )
A1: sin . (x + (PI / 2)) = cos . x by SIN_COS:83;
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:8;
PI / 2 < x by A2, XXREAL_1:4;
then (PI / 2) + (PI / 2) < x + (PI / 2) by XREAL_1:8;
then x + (PI / 2) in ].PI ,(2 * PI ).[ by A3, XXREAL_1:4;
hence cos . x < 0 by A1, Th25; :: thesis: verum