let x be real number ; :: thesis: ( x in ].(PI / 2),((3 / 2) * PI ).[ implies cos . x < 0 )
assume x in ].(PI / 2),((3 / 2) * PI ).[ ; :: thesis: cos . x < 0
then ( PI / 2 < x & x < (3 / 2) * PI ) by XXREAL_1:4;
then ( (PI / 2) + (PI / 2) < x + (PI / 2) & x + (PI / 2) < ((3 / 2) * PI ) + (PI / 2) ) by XREAL_1:8;
then A1: x + (PI / 2) in ].PI ,(2 * PI ).[ by XXREAL_1:4;
sin . (x + (PI / 2)) = cos . x by SIN_COS:83;
hence cos . x < 0 by A1, Th25; :: thesis: verum