let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies sin (angle (A,B,C)) <> 0 )
assume A1: A,B,C is_a_triangle ; :: thesis: sin (angle (A,B,C)) <> 0
assume A2: sin (angle (A,B,C)) = 0 ; :: thesis: contradiction
the_area_of_polygon3 (C,B,A) = ((|.(C - B).| * |.(A - B).|) * (sin (angle (A,B,C)))) / 2 by EUCLID_6:5
.= 0 by A2 ;
then not C,B,A is_a_triangle by MENELAUS:9;
hence contradiction by A1, MENELAUS:15; :: thesis: verum