let A, B, C, A1, B1, C1, A2, B2, C2 be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & A1 = ((2 / 3) * B) + ((1 / 3) * C) & B1 = ((2 / 3) * C) + ((1 / 3) * A) & C1 = ((2 / 3) * A) + ((1 / 3) * B) & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear implies the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7 )
assume that
A1: A,B,C is_a_triangle and
A2: ( A1 = ((2 / 3) * B) + ((1 / 3) * C) & B1 = ((2 / 3) * C) + ((1 / 3) * A) & C1 = ((2 / 3) * A) + ((1 / 3) * B) ) and
A3: ( A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear ) ; :: thesis: the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7
consider lambda, mu, nu being Real such that
A4: ( lambda = 1 / 3 & mu = 1 / 3 & nu = 1 / 3 ) ;
( A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 & 1 - lambda = 2 / 3 & 1 - mu = 2 / 3 & 1 - nu = 2 / 3 ) by A2, A4;
then the_area_of_polygon3 (A2,B2,C2) = ((((((1 / 3) * (1 / 3)) * (1 / 3)) - (((2 / 3) * (2 / 3)) * (2 / 3))) ^2) / ((((2 / 3) + ((1 / 3) * (1 / 3))) * ((2 / 3) + ((1 / 3) * (1 / 3)))) * ((2 / 3) + ((1 / 3) * (1 / 3))))) * (the_area_of_polygon3 (A,B,C)) by Th19, A1, A3;
hence the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7 ; :: thesis: verum