for B, C being Point of (TOP-REAL 2) holds the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = (((B `1) * (C `2)) - ((C `1) * (B `2))) / 2