theorem Thm27: :: EUCLID10:42

for A, B, C being Point of (TOP-REAL 2) holds
( the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (B,C,A) & the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (C,A,B) )