let x be Real; :: thesis: ( x in [.0,PI.] implies sin . x >= 0 )
assume A1: x in [.0,PI.] ; :: thesis: sin . x >= 0
then x <= PI by XXREAL_1:1;
then ( x = 0 or x = PI or ( 0 < x & x < PI ) ) by A1, XXREAL_0:1, XXREAL_1:1;
then ( x = 0 or x = PI or x in ].0,PI.[ ) by XXREAL_1:4;
hence sin . x >= 0 by Th7, SIN_COS:30, SIN_COS:76; :: thesis: verum