let x be Real; :: 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 Th11, SIN_COS:30, SIN_COS:76; :: thesis: verum