let A, B, C, A1, B1, C1, A2, B2, C2 be Point of (TOP-REAL 2); for lambda, mu, nu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear holds
( (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)) <> 0 & the_area_of_polygon3 (A2,B2,C2) = (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * (the_area_of_polygon3 (A,B,C)) )
let lambda, mu, nu be Real; ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear implies ( (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)) <> 0 & the_area_of_polygon3 (A2,B2,C2) = (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * (the_area_of_polygon3 (A,B,C)) ) )
assume that
A1:
A,B,C is_a_triangle
and
A2:
A1 = ((1 - lambda) * B) + (lambda * C)
and
A3:
B1 = ((1 - mu) * C) + (mu * A)
and
A4:
C1 = ((1 - nu) * A) + (nu * B)
and
A5:
lambda <> 1
and
A6:
mu <> 1
and
A7:
nu <> 1
and
A8:
A,A1,B2,C2 are_collinear
and
A9:
B,B1,A2,C2 are_collinear
and
A10:
C,C1,A2,B2 are_collinear
; ( (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)) <> 0 & the_area_of_polygon3 (A2,B2,C2) = (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * (the_area_of_polygon3 (A,B,C)) )
A11:
A,A1,C2 are_collinear
by A8;
A12:
B,B1,C2 are_collinear
by A9;
A13:
B,B1,A2 are_collinear
by A9;
A14:
C,C1,A2 are_collinear
by A10;
A15:
A,A1,B2 are_collinear
by A8;
A16:
C,C1,B2 are_collinear
by A10;
A17:
C,A,B is_a_triangle
by A1;
A18:
B,C,A is_a_triangle
by A1;
set q1 = (1 - mu) + (lambda * mu);
set q2 = (1 - lambda) + (nu * lambda);
set q3 = (1 - nu) + (mu * nu);
consider alpha being Real such that
A19:
C2 = ((1 - alpha) * A) + (alpha * A1)
and
A20:
alpha = (1 - mu) / ((1 - mu) + (lambda * mu))
by Lm2, A1, A2, A3, A6, A11, A12;
A21:
(1 - mu) + (lambda * mu) <> 0
by Lm2, A1, A2, A3, A6, A11, A12;
consider beta being Real such that
A22:
B2 = ((1 - beta) * C) + (beta * C1)
and
A23:
beta = (1 - lambda) / ((1 - lambda) + (nu * lambda))
by Lm2, A17, A4, A2, A5, A16, A15;
A24:
(1 - lambda) + (nu * lambda) <> 0
by Lm2, A17, A4, A2, A5, A16, A15;
consider gamma being Real such that
A25:
A2 = ((1 - gamma) * B) + (gamma * B1)
and
A26:
gamma = (1 - nu) / ((1 - nu) + (mu * nu))
by Lm2, A18, A3, A4, A7, A13, A14;
A27:
(1 - nu) + (mu * nu) <> 0
by Lm2, A18, A3, A4, A7, A13, A14;
1 - alpha = ((1 * ((1 - mu) + (lambda * mu))) - (1 - mu)) / ((1 - mu) + (lambda * mu))
by A20, A21, XCMPLX_1:127;
then A28:
1 - alpha = (lambda * mu) * (1 / ((1 - mu) + (lambda * mu)))
by XCMPLX_1:99;
1 - beta = ((1 * ((1 - lambda) + (nu * lambda))) - (1 - lambda)) / ((1 - lambda) + (nu * lambda))
by A23, A24, XCMPLX_1:127;
then A29:
1 - beta = (nu * lambda) * (1 / ((1 - lambda) + (nu * lambda)))
by XCMPLX_1:99;
1 - gamma = ((1 * ((1 - nu) + (mu * nu))) - (1 - nu)) / ((1 - nu) + (mu * nu))
by A26, A27, XCMPLX_1:127;
then A30:
1 - gamma = (mu * nu) * (1 / ((1 - nu) + (mu * nu)))
by XCMPLX_1:99;
A31:
alpha = (1 - mu) * (1 / ((1 - mu) + (lambda * mu)))
by A20, XCMPLX_1:99;
A32:
beta = (1 - lambda) * (1 / ((1 - lambda) + (nu * lambda)))
by A23, XCMPLX_1:99;
A33:
gamma = (1 - nu) * (1 / ((1 - nu) + (mu * nu)))
by A26, XCMPLX_1:99;
thus
(((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)) <> 0
by A21, A24, A27; the_area_of_polygon3 (A2,B2,C2) = (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * (the_area_of_polygon3 (A,B,C))
set S = the_area_of_polygon3 (A,B,C);
the_area_of_polygon3 (A2,B2,C2) =
((1 - gamma) * (the_area_of_polygon3 (B,B2,C2))) + (gamma * (the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),B2,C2)))
by A3, Th7, A25
.=
((1 - gamma) * (the_area_of_polygon3 (B,B2,C2))) + (gamma * (((1 - mu) * (the_area_of_polygon3 (C,B2,C2))) + (mu * (the_area_of_polygon3 (A,B2,C2)))))
by Th7
.=
(- ((1 - gamma) * (the_area_of_polygon3 (C2,B2,B)))) - (gamma * (((1 - mu) * (the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),C,C2))) + (mu * (the_area_of_polygon3 (C2,B2,A)))))
by A22
.=
(- ((1 - gamma) * (the_area_of_polygon3 (C2,B2,B)))) - (gamma * (((1 - mu) * (((1 - beta) * (the_area_of_polygon3 (C,C,C2))) + (beta * (the_area_of_polygon3 (C1,C,C2))))) + (mu * (the_area_of_polygon3 (C2,B2,A)))))
by Th7
.=
((- ((1 - gamma) * (the_area_of_polygon3 ((((1 - alpha) * A) + (alpha * A1)),B2,B)))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A19
.=
((- ((1 - gamma) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,B))) + (alpha * (the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B2,B)))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A2, Th7
.=
((- ((1 - gamma) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,B))) + (alpha * (((1 - lambda) * (the_area_of_polygon3 (B,B2,B))) + (lambda * (the_area_of_polygon3 (C,B2,B)))))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7
.=
((- ((1 - gamma) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,B))) - ((alpha * lambda) * (the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),C,B)))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A22
.=
((- ((1 - gamma) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,B))) - ((alpha * lambda) * (((1 - beta) * (the_area_of_polygon3 (C,C,B))) + (beta * (the_area_of_polygon3 (C1,C,B)))))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7
.=
((- ((1 - gamma) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,B))) - (((alpha * lambda) * beta) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,B)))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A4
.=
((- ((1 - gamma) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,B))) - (((alpha * lambda) * beta) * (((1 - nu) * (the_area_of_polygon3 (A,C,B))) + (nu * (the_area_of_polygon3 (B,C,B)))))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7
.=
(((1 - gamma) * (((1 - alpha) * (the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),A,B))) - ((((alpha * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A22
.=
(((1 - gamma) * (((1 - alpha) * (((1 - beta) * (the_area_of_polygon3 (C,A,B))) + (beta * (the_area_of_polygon3 (C1,A,B))))) - ((((alpha * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7
.=
(((1 - gamma) * (((1 - alpha) * (((1 - beta) * (the_area_of_polygon3 (A,B,C))) + (beta * (((1 - nu) * (the_area_of_polygon3 (A,A,B))) + (nu * (the_area_of_polygon3 (B,A,B))))))) - ((((alpha * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7, A4
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * (((1 - nu) * (the_area_of_polygon3 (A,C,C2))) + (nu * (the_area_of_polygon3 (B,C,C2)))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7, A4
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * (((1 - nu) * (the_area_of_polygon3 ((((1 - alpha) * A) + (alpha * A1)),A,C))) + (nu * (the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A19
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * (((1 - nu) * (((1 - alpha) * (the_area_of_polygon3 (A,A,C))) + (alpha * (the_area_of_polygon3 (A1,A,C))))) + (nu * (the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * ((((1 - nu) * alpha) * (the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),A,C))) + (nu * (the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A2
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * ((((1 - nu) * alpha) * (((1 - lambda) * (the_area_of_polygon3 (B,A,C))) + (lambda * (the_area_of_polygon3 (C,A,C))))) + (nu * (the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * ((- ((((1 - nu) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C)))) + (nu * (((1 - alpha) * (the_area_of_polygon3 (A,B,C))) + (alpha * (the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B,C)))))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by A2, Th7, A19
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * ((- ((((1 - nu) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C)))) + (nu * (((1 - alpha) * (the_area_of_polygon3 (A,B,C))) + (alpha * (((1 - lambda) * (the_area_of_polygon3 (B,B,C))) + (lambda * (the_area_of_polygon3 (C,B,C)))))))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A)))
by Th7
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - ((gamma * mu) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,A))) + (alpha * (the_area_of_polygon3 (A1,B2,A)))))
by Th7, A19
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * (the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B2,A)))
by A2
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * (((1 - lambda) * (the_area_of_polygon3 (B,B2,A))) + (lambda * (the_area_of_polygon3 (C,B2,A)))))
by Th7
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * (((1 - lambda) * (the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),A,B))) + (lambda * (the_area_of_polygon3 (B2,A,C)))))
by A22
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * (((1 - lambda) * (((1 - beta) * (the_area_of_polygon3 (C,A,B))) + (beta * (the_area_of_polygon3 (C1,A,B))))) + (lambda * (the_area_of_polygon3 (B2,A,C)))))
by Th7
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * (((1 - lambda) * (((1 - beta) * (the_area_of_polygon3 (A,B,C))) + (beta * (((1 - nu) * (the_area_of_polygon3 (A,A,B))) + (nu * (the_area_of_polygon3 (B,A,B))))))) + (lambda * (the_area_of_polygon3 (B2,A,C)))))
by Th7, A4
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) + (lambda * (((1 - beta) * (the_area_of_polygon3 (C,A,C))) + (beta * (the_area_of_polygon3 (C1,A,C)))))))
by Th7, A22
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) + ((lambda * beta) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),A,C)))))
by A4
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) + ((lambda * beta) * (((1 - nu) * (the_area_of_polygon3 (A,A,C))) + (nu * (the_area_of_polygon3 (B,A,C)))))))
by Th7
.=
((((((1 - gamma) * (1 - alpha)) * (1 - beta)) - (((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu))) + ((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) - ((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)))) + ((((((gamma * mu) * alpha) * lambda) * beta) * nu) - ((((gamma * mu) * alpha) * (1 - lambda)) * (1 - beta)))) * (the_area_of_polygon3 (A,B,C))
.=
(((((((mu * nu) * (1 / ((1 - nu) + (mu * nu)))) * ((lambda * mu) * (1 / ((1 - mu) + (lambda * mu))))) * ((nu * lambda) * (1 / ((1 - lambda) + (nu * lambda))))) - ((((((mu * nu) * (1 / ((1 - nu) + (mu * nu)))) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * lambda) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * (1 - nu))) + ((((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * (1 - mu)) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * (1 - nu)) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * (1 - lambda)) - ((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * (1 - mu)) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * nu) * ((lambda * mu) * (1 / ((1 - mu) + (lambda * mu))))))) + ((((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * mu) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * lambda) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * nu) - ((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * mu) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * (1 - lambda)) * ((nu * lambda) * (1 / ((1 - lambda) + (nu * lambda))))))) * (the_area_of_polygon3 (A,B,C))
by A28, A31, A29, A32, A30, A33
.=
(((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) * (((1 / ((1 - mu) + (lambda * mu))) * (1 / ((1 - lambda) + (nu * lambda)))) * (1 / ((1 - nu) + (mu * nu))))) * (the_area_of_polygon3 (A,B,C))
.=
(((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) * ((1 / (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda)))) * (1 / ((1 - nu) + (mu * nu))))) * (the_area_of_polygon3 (A,B,C))
by XCMPLX_1:102
.=
(((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) * (1 / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu))))) * (the_area_of_polygon3 (A,B,C))
by XCMPLX_1:102
;
hence
the_area_of_polygon3 (A2,B2,C2) = (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * (the_area_of_polygon3 (A,B,C))
by XCMPLX_1:99; verum