theorem Th22: :: EUCLID_6:22

for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) st p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & angle (p1,p2,p3) = angle (p4,p5,p6) & angle (p3,p1,p2) = angle (p5,p6,p4) holds
( |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| & |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| )