let p2, p1, p3 be Point of (TOP-REAL 2); :: thesis: ( p2 <> p1 implies |.(p3 - p2).| * (sin (angle p3,p2,p1)) = |.(p3 - p1).| * (sin (angle p2,p1,p3)) )
assume p2 <> p1 ; :: thesis: |.(p3 - p2).| * (sin (angle p3,p2,p1)) = |.(p3 - p1).| * (sin (angle p2,p1,p3))
then A1: |.(p1 - p2).| <> 0 by Lm1;
the_area_of_polygon3 p1,p2,p3 = the_area_of_polygon3 p3,p1,p2 ;
then ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2 = the_area_of_polygon3 p3,p1,p2 by Th5;
then ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2 = ((|.(p3 - p1).| * |.(p2 - p1).|) * (sin (angle p2,p1,p3))) / 2 by Th5;
then (|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1)) = (|.(p3 - p1).| * |.(p1 - p2).|) * (sin (angle p2,p1,p3)) by Lm2;
then (|.(p3 - p2).| * (sin (angle p3,p2,p1))) * |.(p1 - p2).| = (|.(p3 - p1).| * (sin (angle p2,p1,p3))) * |.(p1 - p2).| ;
hence |.(p3 - p2).| * (sin (angle p3,p2,p1)) = |.(p3 - p1).| * (sin (angle p2,p1,p3)) by A1, XCMPLX_1:5; :: thesis: verum