for A, B, C, A1, B1, C1, A2, B2, C2 being Point of (TOP-REAL 2) st 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 holds
the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7