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: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 Th29, SIN_COS:81; :: thesis: verum