let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2

per cases ( p1 = p2 or p1 <> p2 ) ;

suppose A1: p1 = p2 ; :: thesis: the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2

then |.(p1 - p2).| = |.(0. (TOP-REAL 2)).| by EUCLID:46
.= 0 by EUCLID_2:61 ;
hence the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2 by A1; :: thesis: verum

end;

suppose A2: p1 <> p2 ; :: thesis: the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2

per cases ( p2 = p3 or p2 <> p3 ) ;

suppose A3: p2 = p3 ; :: thesis: the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2

then |.(p3 - p2).| = |.(0. (TOP-REAL 2)).| by EUCLID:46
.= 0 by EUCLID_2:61 ;
hence the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2 by A3; :: thesis: verum

end;

suppose A4: p2 <> p3 ; :: thesis: the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2

set b = euc2cpx (p3 - p2);
set a = euc2cpx (p1 - p2);

A5: now

assume A6: ( euc2cpx (p1 - p2) = 0 or euc2cpx (p3 - p2) = 0 ) ; :: thesis: contradiction

per cases ( euc2cpx (p1 - p2) = 0 or euc2cpx (p3 - p2) = 0 ) by A6;

suppose euc2cpx (p1 - p2) = 0 ; :: thesis: contradiction

hence contradiction by A2, EUCLID:47, EUCLID_3:22; :: thesis: verum

end;

suppose euc2cpx (p3 - p2) = 0 ; :: thesis: contradiction

hence contradiction by A4, EUCLID:47, EUCLID_3:22; :: thesis: verum

end;

end;

end;

A7: now

assume A8: |.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).| = 0 ; :: thesis: contradiction

per cases ( |.(euc2cpx (p1 - p2)).| = 0 or |.(euc2cpx (p3 - p2)).| = 0 ) by A8;

suppose |.(euc2cpx (p1 - p2)).| = 0 ; :: thesis: contradiction

hence contradiction by A5, COMPLEX1:131; :: thesis: verum

end;

suppose |.(euc2cpx (p3 - p2)).| = 0 ; :: thesis: contradiction

hence contradiction by A5, COMPLEX1:131; :: thesis: verum

end;

end;

end;

((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (- (sin (angle p1,p2,p3)))) / 2 by Th2
.= ((|.(p1 - p2).| * |.(p3 - p2).|) * (- (sin (angle (euc2cpx (p1 - p2)),(euc2cpx (p3 - p2)))))) / 2 by Lm7
.= ((|.(p1 - p2).| * |.(p3 - p2).|) * (- (- ((Im ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|))))) / 2 by A5, COMPLEX2:83
.= ((|.(euc2cpx (p1 - p2)).| * |.(p3 - p2).|) * ((Im ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|))) / 2 by Lm16
.= ((|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|) * ((Im ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|))) / 2 by Lm16
.= ((Im ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / ((|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|) / (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|))) / 2 by XCMPLX_1:82
.= ((Im ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / 1) / 2 by A7, XCMPLX_1:60
.= ((- (((p1 `1 ) - (p2 `1 )) * ((p3 `2 ) - (p2 `2 )))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `1 ) - (p2 `1 )))) / 2 by Lm16
.= (((((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 ;
hence the_area_of_polygon3 p1,p2,p3 = ((|.(p1 - p2).| * |.(p3 - p2).|) * (sin (angle p3,p2,p1))) / 2 ; :: thesis: verum

end;

end;

end;

end;