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 RLVECT_1:5
.= 0 by EUCLID_2:39 ;
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 RLVECT_1:5
.= 0 by EUCLID_2:39 ;
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 :: thesis: ( not euc2cpx (p1 - p2) = 0 & not euc2cpx (p3 - p2) = 0 )

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_3:18, RLVECT_1:21; :: thesis: verum

end;

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

hence contradiction by A4, EUCLID_3:18, RLVECT_1:21; :: thesis: verum

end;

end;

end;

A7: now :: thesis: not |.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).| = 0

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:45; :: thesis: verum

end;

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

hence contradiction by A5, COMPLEX1:45; :: 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:69
.= ((|.(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:81
.= ((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;