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 A2: x in ].0 ,(PI / 2).[ ; :: thesis: sin . x > 0

then x < PI / 2 by XXREAL_1:4;
then - x > - (PI / 2) by XREAL_1:26;
then A3: (- x) + (PI / 2) > (- (PI / 2)) + (PI / 2) by XREAL_1:8;
0 < x by A2, XXREAL_1:4;
then (- x) + (PI / 2) < 0 + (PI / 2) by XREAL_1:8;
then (PI / 2) - x in ].0 ,(PI / 2).[ by A3, 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 A4: x in ].(PI / 2),PI .[ ; :: thesis: sin . x > 0

then x < PI by XXREAL_1:4;
then A5: x - (PI / 2) < PI - (PI / 2) by XREAL_1:11;
PI / 2 < x by A4, XXREAL_1:4;
then (PI / 2) - (PI / 2) < x - (PI / 2) by XREAL_1:11;
then x - (PI / 2) in ].0 ,(PI / 2).[ by A5, 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;