let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: for a, b, c, s being Real st a = |.(p2 - p1).| & b = |.(p3 - p2).| & c = |.(p1 - p3).| & s = (the_perimeter_of_polygon3 (p1,p2,p3)) / 2 holds
|.(the_area_of_polygon3 (p1,p2,p3)).| = sqrt (((s * (s - a)) * (s - b)) * (s - c))
let a, b, c, s be Real; :: thesis: ( a = |.(p2 - p1).| & b = |.(p3 - p2).| & c = |.(p1 - p3).| & s = (the_perimeter_of_polygon3 (p1,p2,p3)) / 2 implies |.(the_area_of_polygon3 (p1,p2,p3)).| = sqrt (((s * (s - a)) * (s - b)) * (s - c)) )
assume that
A1: a = |.(p2 - p1).| and
A2: b = |.(p3 - p2).| and
A3: c = |.(p1 - p3).| ; :: thesis: ( not s = (the_perimeter_of_polygon3 (p1,p2,p3)) / 2 or |.(the_area_of_polygon3 (p1,p2,p3)).| = sqrt (((s * (s - a)) * (s - b)) * (s - c)) )
A4: a = |.(p1 - p2).| by A1, Lm2;
c = |.(p3 - p1).| by A3, Lm2;
then A5: c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3)))) by A2, A4, Th7;
assume A6: s = (the_perimeter_of_polygon3 (p1,p2,p3)) / 2 ; :: thesis: |.(the_area_of_polygon3 (p1,p2,p3)).| = sqrt (((s * (s - a)) * (s - b)) * (s - c))
A7: ((sin (angle (p3,p2,p1))) ^2) + ((cos (angle (p3,p2,p1))) ^2) = 1 by SIN_COS:29;
(the_area_of_polygon3 (p1,p2,p3)) ^2 = (((a * b) * (sin (angle (p3,p2,p1)))) / 2) ^2 by A2, A4, 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 A7, SQUARE_1:9
.= (((((a * b) ^2) - (((a * b) ^2) * ((cos (angle (p3,p2,p1))) ^2))) * (2 ^2)) / (2 ^2)) * ((1 / 2) ^2) by XCMPLX_1:89
.= ((((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 A5, Th3
.= ((((16 * (s - a)) * (s - b)) * ((s - c) * s)) / (2 * 2)) * ((1 / 2) ^2) by A1, A2, A3, A6
.= ((s * (s - a)) * (s - b)) * (s - c) ;
hence |.(the_area_of_polygon3 (p1,p2,p3)).| = sqrt (((s * (s - a)) * (s - b)) * (s - c)) by COMPLEX1:72; :: thesis: verum