theorem
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