let p2, p1, p3 be Point of (TOP-REAL 2); :: thesis: for a, b, c, s being real number st a = |.(p2 - p1).| & b = |.(p3 - p2).| & c = |.(p1 - p3).| & s = (the_perimeter_of_polygon3 p1,p2,p3) / 2 holds
abs (the_area_of_polygon3 p1,p2,p3) = sqrt (((s * (s - a)) * (s - b)) * (s - c))
let a, b, c, s be real number ; :: thesis: ( a = |.(p2 - p1).| & b = |.(p3 - p2).| & c = |.(p1 - p3).| & s = (the_perimeter_of_polygon3 p1,p2,p3) / 2 implies abs (the_area_of_polygon3 p1,p2,p3) = sqrt (((s * (s - a)) * (s - b)) * (s - c)) )
assume A1: ( a = |.(p2 - p1).| & b = |.(p3 - p2).| & c = |.(p1 - p3).| ) ; :: thesis: ( not s = (the_perimeter_of_polygon3 p1,p2,p3) / 2 or abs (the_area_of_polygon3 p1,p2,p3) = sqrt (((s * (s - a)) * (s - b)) * (s - c)) )
assume A2: s = (the_perimeter_of_polygon3 p1,p2,p3) / 2 ; :: thesis: abs (the_area_of_polygon3 p1,p2,p3) = sqrt (((s * (s - a)) * (s - b)) * (s - c))
A3: a = |.(p1 - p2).| by A1, Lm2;
A4: c = |.(p3 - p1).| by A1, Lm2;
A5: ((sin (angle p3,p2,p1)) ^2 ) + ((cos (angle p3,p2,p1)) ^2 ) = 1 by SIN_COS:32;
A6: c ^2 = ((a ^2 ) + (b ^2 )) - (((2 * a) * b) * (cos (angle p1,p2,p3))) by A1, A3, A4, Th7;
(the_area_of_polygon3 p1,p2,p3) ^2 = (((a * b) * (sin (angle p3,p2,p1))) / 2) ^2 by A1, A3, Th5
.= (((a * b) * (sin (angle p3,p2,p1))) ^2 ) * ((1 / 2) ^2 )
.= (((a * b) ^2 ) * (1 - ((cos (angle p3,p2,p1)) ^2 ))) * ((1 / 2) ^2 ) by A5, SQUARE_1:68
.= (((((a * b) ^2 ) - (((a * b) ^2 ) * ((cos (angle p3,p2,p1)) ^2 ))) * (2 ^2 )) / (2 ^2 )) * ((1 / 2) ^2 ) by XCMPLX_1:90
.= ((((2 ^2 ) * ((a * b) ^2 )) - ((((2 * a) * b) * (cos (angle p3,p2,p1))) ^2 )) / (2 ^2 )) * ((1 / 2) ^2 )
.= ((((2 ^2 ) * ((a * b) ^2 )) - ((((- (c ^2 )) + (a ^2 )) + (b ^2 )) ^2 )) / (2 ^2 )) * ((1 / 2) ^2 ) by A6, Th3
.= ((((16 * (s - a)) * (s - b)) * ((s - c) * s)) / (2 * 2)) * ((1 / 2) ^2 ) by A1, A2
.= ((s * (s - a)) * (s - b)) * (s - c) ;
hence abs (the_area_of_polygon3 p1,p2,p3) = sqrt (((s * (s - a)) * (s - b)) * (s - c)) by COMPLEX1:158; :: thesis: verum