let x be real number ; :: thesis: ( x in ].0 ,PI .[ implies sin . x > 0 )
assume A1: x in ].0 ,PI .[ ; :: thesis: sin . x > 0

per cases ( x in ].0 ,(PI / 2).[ or x = PI / 2 or x in ].(PI / 2),PI .[ ) by A1, Th22;

suppose x in ].0 ,(PI / 2).[ ; :: thesis: sin . x > 0

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

end;

suppose x = PI / 2 ; :: thesis: sin . x > 0

hence sin . x > 0 by SIN_COS:81; :: thesis: verum

end;

suppose x in ].(PI / 2),PI .[ ; :: thesis: sin . x > 0

then ( PI / 2 < x & x < PI ) by XXREAL_1:4;
then ( (PI / 2) - (PI / 2) < x - (PI / 2) & x - (PI / 2) < PI - (PI / 2) ) by XREAL_1:11;
then x - (PI / 2) in ].0 ,(PI / 2).[ by XXREAL_1:4;
then cos . (- ((PI / 2) - x)) > 0 by SIN_COS:85;
then cos . ((PI / 2) - x) > 0 by SIN_COS:33;
hence sin . x > 0 by SIN_COS:83; :: thesis: verum

end;

end;