let x be Real; :: 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:1;
then ( x = PI / 2 or x = (3 / 2) * PI or ( PI / 2 < x & x < (3 / 2) * PI ) ) by XXREAL_0:1;
then ( x = PI / 2 or x = (3 / 2) * PI or x in ].(PI / 2),((3 / 2) * PI).[ ) by XXREAL_1:4;
hence cos . x <= 0 by Th13, SIN_COS:76; :: thesis: verum