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