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: ( 0 <= th & 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 A3: 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
A5: ( r in ].0 ,th.[ & diff sin ,r = ((sin . th) - (sin . 0 )) / (th - 0 ) ) by A3, Th73, Th27, FDIFF_1:34, ROLLE:3;
( 0 < r & r < th ) by A5, XXREAL_1:4;
then ( 0 < r & r < 1 ) by A2, XXREAL_0:2;
then r in [.0 ,1.] by XXREAL_1:1;
then A7: cos . r > 0 by Th74;
(sin . th) - (sin . 0 ) > 0 by A3, A7, A5, 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