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