theorem :: MENELAUS:11

for A, B, C, A1 being Point of (TOP-REAL 2) holds the_area_of_polygon3 ((A + A1),B,C) = ((the_area_of_polygon3 (A,B,C)) + (the_area_of_polygon3 (A1,B,C))) - (the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C))