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