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

proof

A4: now

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

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

thus sin . th >= sin . 0 by A5; :: thesis: verum

end;

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

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

end;

end;

end;

thus sin . th >= sin . 0 by A4; :: thesis: verum

end;

thus sin . th >= 0 by A3, Th33; :: thesis: verum