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:4;
then ( (- (PI / 2)) + (PI / 2) < x + (PI / 2) & x + (PI / 2) < (PI / 2) + (PI / 2) ) by XREAL_1:8;
then A1: x + (PI / 2) in ].0 ,PI .[ by XXREAL_1:4;
sin . (x + (PI / 2)) = cos . x by SIN_COS:83;
hence cos . x > 0 by A1, Th23; :: thesis: verum