let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies sin ((angle (A,B,C)) / 2) > 0 )
assume A1: A,B,C is_a_triangle ; :: thesis: sin ((angle (A,B,C)) / 2) > 0
( 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI ) by EUCLID11:2;
then ( 0 < angle (A,B,C) & angle (A,B,C) < 2 * PI ) by A1, EUCLID10:30;
then ( 0 / 2 < (angle (A,B,C)) / 2 & (angle (A,B,C)) / 2 < (2 * PI) / 2 ) by XREAL_1:74;
then ( (2 * PI) * 0 < (angle (A,B,C)) / 2 & (angle (A,B,C)) / 2 < PI + ((2 * PI) * 0) ) ;
hence sin ((angle (A,B,C)) / 2) > 0 by SIN_COS6:11; :: thesis: verum