theorem Th5: :: EUCLID_6:5

for p1, p2, p3 being Point of (TOP-REAL 2) holds the_area_of_polygon3 (p1,p2,p3) = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle (p3,p2,p1)))) / 2