let A, B, C, A1, B1, C2 be Point of (TOP-REAL 2); :: thesis: for lambda, mu, alpha being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C2 = ((1 - alpha) * A) + (alpha * A1) holds
the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C))
let lambda, mu, alpha be Real; :: thesis: ( A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C2 = ((1 - alpha) * A) + (alpha * A1) implies the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C)) )
assume that
A1: A1 = ((1 - lambda) * B) + (lambda * C) and
A2: B1 = ((1 - mu) * C) + (mu * A) and
A3: C2 = ((1 - alpha) * A) + (alpha * A1) ; :: thesis: the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C))
the_area_of_polygon3 (B,B1,C2) = the_area_of_polygon3 ((((1 - alpha) * A) + (alpha * A1)),B,B1) by A3
.= ((1 - alpha) * (the_area_of_polygon3 (A,B,B1))) + (alpha * (the_area_of_polygon3 (A1,B,B1))) by Th7
.= ((1 - alpha) * (the_area_of_polygon3 (B1,A,B))) + (alpha * (((1 - lambda) * (the_area_of_polygon3 (B,B,B1))) + (lambda * (the_area_of_polygon3 (C,B,B1))))) by Th7, A1
.= ((1 - alpha) * (((1 - mu) * (the_area_of_polygon3 (C,A,B))) + (mu * (the_area_of_polygon3 (A,A,B))))) + ((alpha * lambda) * (the_area_of_polygon3 (B1,C,B))) by Th7, A2
.= (((1 - alpha) * (1 - mu)) * (the_area_of_polygon3 (C,A,B))) + ((alpha * lambda) * (((1 - mu) * (the_area_of_polygon3 (C,C,B))) + (mu * (the_area_of_polygon3 (A,C,B))))) by Th7, A2
.= (((1 - alpha) * (1 - mu)) * (the_area_of_polygon3 (A,B,C))) - (((alpha * lambda) * mu) * (the_area_of_polygon3 (A,B,C))) ;
hence the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C)) ; :: thesis: verum