theorem Thm28: :: EUCLID10:43

for A, B, C being Point of (TOP-REAL 2) holds the_area_of_polygon3 (A,B,C) = - (the_area_of_polygon3 (B,A,C))