:: deftheorem defines the_area_of_polygon3 EUCLID_6:def 1 :
for p1, p2, p3 being Point of (TOP-REAL 2) holds the_area_of_polygon3 (p1,p2,p3) = (((((p1 `1) * (p2 `2)) - ((p2 `1) * (p1 `2))) + (((p2 `1) * (p3 `2)) - ((p3 `1) * (p2 `2)))) + (((p3 `1) * (p1 `2)) - ((p1 `1) * (p3 `2)))) / 2;