let x be Real; :: 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, Th6;
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:24;
then A3: (- x) + (PI / 2) > (- (PI / 2)) + (PI / 2) by XREAL_1:6;
0 < x by A2, XXREAL_1:4;
then (- x) + (PI / 2) < 0 + (PI / 2) by XREAL_1:6;
then (PI / 2) - x in ].0,(PI / 2).[ by A3, XXREAL_1:4;
then cos . ((PI / 2) - x) > 0 by SIN_COS:80;
hence sin . x > 0 by SIN_COS:78; :: thesis: verum
end;
suppose x = PI / 2 ; :: thesis: sin . x > 0
hence sin . x > 0 by SIN_COS:76; :: 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:9;
PI / 2 < x by A4, XXREAL_1:4;
then (PI / 2) - (PI / 2) < x - (PI / 2) by XREAL_1:9;
then x - (PI / 2) in ].0,(PI / 2).[ by A5, XXREAL_1:4;
then cos . (- ((PI / 2) - x)) > 0 by SIN_COS:80;
then cos . ((PI / 2) - x) > 0 by SIN_COS:30;
hence sin . x > 0 by SIN_COS:78; :: thesis: verum
end;
end;