let th be real number ; :: thesis: ( th in ].0 ,(PI / 2).[ implies 0 < sin . th )
assume th in ].0 ,(PI / 2).[ ; :: thesis: 0 < sin . th
then ( 0 < th & th < PI / 2 ) by XXREAL_1:4;
then ( 0 - th < 0 & - th > - (PI / 2) ) by XREAL_1:26;
then ( (- th) + (PI / 2) < 0 + (PI / 2) & (- th) + (PI / 2) > (- (PI / 2)) + (PI / 2) ) by XREAL_1:8;
then (PI / 2) - th in ].0 ,(PI / 2).[ by XXREAL_1:4;
then cos . ((PI / 2) - th) > 0 by SIN_COS:85;
hence 0 < sin . th by SIN_COS:83; :: thesis: verum