let A, B, C be Point of (TOP-REAL 2); :: thesis: ( angle (C,B,A) < PI implies 0 <= the_area_of_polygon3 (A,B,C) )
assume angle (C,B,A) < PI ; :: thesis: 0 <= the_area_of_polygon3 (A,B,C)
then ( (2 * PI) * 0 <= angle (C,B,A) & angle (C,B,A) < PI + ((2 * PI) * 0) ) by Th2;
then A1: sin (angle (C,B,A)) >= 0 by SIN_COS6:16;
the_area_of_polygon3 (A,B,C) = ((|.(A - B).| * |.(C - B).|) * (sin (angle (C,B,A)))) / 2 by EUCLID_6:5;
hence 0 <= the_area_of_polygon3 (A,B,C) by A1; :: thesis: verum