:: deftheorem defines the_perimeter_of_polygon3 EUCLID_6:def 2 :
for p1, p2, p3 being Point of (TOP-REAL 2) holds the_perimeter_of_polygon3 (p1,p2,p3) = (|.(p2 - p1).| + |.(p3 - p2).|) + |.(p1 - p3).|;