let p1, p2, 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))) )
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 A1: (|.(p3 - p2).| * (sin (angle (p3,p2,p1)))) * |.(p1 - p2).| = (|.(p3 - p1).| * (sin (angle (p2,p1,p3)))) * |.(p1 - p2).| ;
assume p2 <> p1 ; :: thesis: |.(p3 - p2).| * (sin (angle (p3,p2,p1))) = |.(p3 - p1).| * (sin (angle (p2,p1,p3)))
then |.(p1 - p2).| <> 0 by Lm1;
hence |.(p3 - p2).| * (sin (angle (p3,p2,p1))) = |.(p3 - p1).| * (sin (angle (p2,p1,p3))) by A1, XCMPLX_1:5; :: thesis: verum