let x be Real; :: thesis: ( x in [.((3 / 2) * PI),(2 * PI).] implies cos . x >= 0 )
assume x in [.((3 / 2) * PI),(2 * PI).] ; :: thesis: cos . x >= 0
then ( (3 / 2) * PI <= x & x <= 2 * PI ) by XXREAL_1:1;
then ( x = (3 / 2) * PI or x = 2 * PI or ( (3 / 2) * PI < x & x < 2 * PI ) ) by XXREAL_0:1;
then ( x = (3 / 2) * PI or x = 2 * PI or x in ].((3 / 2) * PI),(2 * PI).[ ) by XXREAL_1:4;
hence cos . x >= 0 by Th15, SIN_COS:76; :: thesis: verum