let x be real number ; :: thesis: ( x in [.0 ,PI .] implies sin . x >= 0 )
assume x in [.0 ,PI .] ; :: thesis: sin . x >= 0
then ( 0 <= x & x <= PI ) by XXREAL_1:1;
then ( x = 0 or x = PI or ( 0 < x & x < PI ) ) by XXREAL_0:1;
then ( x = 0 or x = PI or x in ].0 ,PI .[ ) by XXREAL_1:4;
hence sin . x >= 0 by Th23, SIN_COS:33, SIN_COS:81; :: thesis: verum