let B, C be Point of (TOP-REAL 2); :: thesis: the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = (((B `1) * (C `2)) - ((C `1) * (B `2))) / 2
the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = ((((0 * (B `2)) - ((B `1) * (|[0,0]| `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (|[0,0]| `2)) - ((|[0,0]| `1) * (C `2)))) / 2 by EUCLID:52, EUCLID:54
.= (((0 - ((B `1) * 0)) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (|[0,0]| `2)) - ((|[0,0]| `1) * (C `2)))) / 2 by EUCLID:52
.= ((((B `1) * (C `2)) - ((C `1) * (B `2))) + (((C `1) * 0) - ((|[0,0]| `1) * (C `2)))) / 2 by EUCLID:52
.= ((((B `1) * (C `2)) - ((C `1) * (B `2))) + (0 - (0 * (C `2)))) / 2 by EUCLID:52 ;
hence the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = (((B `1) * (C `2)) - ((C `1) * (B `2))) / 2 ; :: thesis: verum