let x be real number ; :: thesis: ( x in [.(- (PI / 2)),(PI / 2).] implies cos . x >= 0 )
assume x in [.(- (PI / 2)),(PI / 2).] ; :: thesis: cos . x >= 0
then ( - (PI / 2) <= x & x <= PI / 2 ) by XXREAL_1:1;
then ( x = - (PI / 2) or x = PI / 2 or ( - (PI / 2) < x & x < PI / 2 ) ) by XXREAL_0:1;
then ( x = - (PI / 2) or x = PI / 2 or x in ].(- (PI / 2)),(PI / 2).[ ) by XXREAL_1:4;
hence cos . x >= 0 by Th27, SIN_COS:33, SIN_COS:81; :: thesis: verum