let A, B, C be Point of (TOP-REAL 2); :: thesis: the_area_of_polygon3 (A,B,C) = - (the_area_of_polygon3 (B,A,C))
A1: the_area_of_polygon3 (A,B,C) = (((((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (A `2)) - ((A `1) * (C `2)))) / 2 by EUCLID_6:def 1;
the_area_of_polygon3 (B,A,C) = (((((B `1) * (A `2)) - ((A `1) * (B `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2)))) + (((C `1) * (B `2)) - ((B `1) * (C `2)))) / 2 by EUCLID_6:def 1;
hence the_area_of_polygon3 (A,B,C) = - (the_area_of_polygon3 (B,A,C)) by A1; :: thesis: verum