let B, C be Point of (TOP-REAL 2); 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
; verum