let th be real number ; :: thesis: ( th in [.0 ,1.] implies sin . th >= 0 )
assume A1: th in [.0 ,1.] ; :: thesis: sin . th >= 0
then A2: th <= 1 by XXREAL_1:1;
sin . th >= sin . 0

proof

now

per cases ( th = 0 or 0 < th ) by A1, XXREAL_1:1;

suppose th = 0 ; :: thesis: sin . th >= sin . 0

hence sin . th >= sin . 0 ; :: thesis: verum

end;

suppose A6: 0 < th ; :: thesis: sin . th >= sin . 0

sin | REAL is continuous by Th73, FDIFF_1:33;
then sin | [.0 ,th.] is continuous by FCONT_1:17;
then consider r being Real such that
A9: r in ].0 ,th.[ and
A10: diff sin ,r = ((sin . th) - (sin . 0 )) / (th - 0 ) by A6, Th27, Th73, FDIFF_1:34, ROLLE:3;
A11: r < th by A9, XXREAL_1:4;
A12: 0 < r by A9, XXREAL_1:4;
r < 1 by A2, A11, XXREAL_0:2;
then r in [.0 ,1.] by A12, XXREAL_1:1;
then cos . r > 0 by Th74;
then (sin . th) - (sin . 0 ) > 0 by A6, A10, Th73;
hence sin . th >= sin . 0 by XREAL_1:49; :: thesis: verum

end;

end;

end;

hence sin . th >= sin . 0 ; :: thesis: verum

end;

hence sin . th >= 0 by Th33; :: thesis: verum