theorem Th7: :: MENELAUS:7

for A, B, C, A1 being Point of (TOP-REAL 2)
for lambda being Real holds the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C) = ((1 - lambda) * (the_area_of_polygon3 (A,B,C))) + (lambda * (the_area_of_polygon3 (A1,B,C)))