let x be Real; :: thesis: ( x in ].(- (PI / 2)),(PI / 2).[ implies cos . x > 0 )
A1: sin . (x + (PI / 2)) = cos . x by SIN_COS:78;
assume A2: x in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: cos . x > 0
then x < PI / 2 by XXREAL_1:4;
then A3: x + (PI / 2) < (PI / 2) + (PI / 2) by XREAL_1:6;
- (PI / 2) < x by A2, XXREAL_1:4;
then (- (PI / 2)) + (PI / 2) < x + (PI / 2) by XREAL_1:6;
then x + (PI / 2) in ].0,PI.[ by A3, XXREAL_1:4;
hence cos . x > 0 by A1, Th7; :: thesis: verum