theorem Th5: :: EUCLID11:10

for A, B, C being Point of (TOP-REAL 2) st angle (C,B,A) < PI holds
0 <= the_area_of_polygon3 (A,B,C)