let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 2); :: thesis: ( 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 implies ( |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| & |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| ) )
assume p1,p2,p3 is_a_triangle ; :: thesis: ( not p4,p5,p6 is_a_triangle or not angle p1,p2,p3 = angle p4,p5,p6 or not angle p3,p1,p2 = angle p5,p6,p4 or ( |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| & |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| ) )
then A1: ( p1,p2,p3 are_mutually_different & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI ) by Th20;
then A2: ( p3 <> p2 & p3 <> p1 & p2 <> p1 ) by ZFMISC_1:def 5;
assume p4,p5,p6 is_a_triangle ; :: thesis: ( not angle p1,p2,p3 = angle p4,p5,p6 or not angle p3,p1,p2 = angle p5,p6,p4 or ( |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| & |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| ) )
then A3: ( p4,p5,p6 are_mutually_different & angle p4,p5,p6 <> PI & angle p5,p6,p4 <> PI & angle p6,p4,p5 <> PI ) by Th20;
then A4: ( p4 <> p5 & p4 <> p6 & p5 <> p6 ) by ZFMISC_1:def 5;
assume A5: ( angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p5,p6,p4 ) ; :: thesis: ( |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| & |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| )
A6: ( euc2cpx p3 <> euc2cpx p2 & euc2cpx p3 <> euc2cpx p1 & euc2cpx p2 <> euc2cpx p1 ) by A2, EUCLID_3:6;
A7: ( euc2cpx p4 <> euc2cpx p5 & euc2cpx p4 <> euc2cpx p6 & euc2cpx p5 <> euc2cpx p6 ) by A4, EUCLID_3:6;
A8: angle p2,p3,p1 = angle p6,p4,p5

proof

per cases ( ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = PI ) or ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = 5 * PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = 5 * PI ) or ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = 5 * PI ) or ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = 5 * PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = PI ) ) by A6, A7, COMPLEX2:102;

suppose ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = PI ) ; :: thesis: angle p2,p3,p1 = angle p6,p4,p5

hence angle p2,p3,p1 = angle p6,p4,p5 by A5; :: thesis: verum

end;

suppose ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = 5 * PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = 5 * PI ) ; :: thesis: angle p2,p3,p1 = angle p6,p4,p5

hence angle p2,p3,p1 = angle p6,p4,p5 by A5; :: thesis: verum

end;

suppose ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = 5 * PI ) ; :: thesis: angle p2,p3,p1 = angle p6,p4,p5

then A9: (angle p2,p3,p1) - (angle p6,p4,p5) = - (4 * PI ) by A5;
A10: ( angle p2,p3,p1 >= 0 & angle p6,p4,p5 < 2 * PI ) by COMPLEX2:84;
then - (angle p6,p4,p5) > - (2 * PI ) by XREAL_1:26;
then (angle p2,p3,p1) + (- (angle p6,p4,p5)) > 0 + (- (2 * PI )) by A10, XREAL_1:10;
then 4 * PI < 2 * PI by A9, XREAL_1:26;
then (4 * PI ) / PI < (2 * PI ) / PI by XREAL_1:76;
then 4 < (2 * PI ) / PI by XCMPLX_1:90;
then 4 < 2 by XCMPLX_1:90;
hence angle p2,p3,p1 = angle p6,p4,p5 ; :: thesis: verum

end;

suppose A11: ( ((angle p3,p1,p2) + (angle p1,p2,p3)) + (angle p2,p3,p1) = 5 * PI & ((angle p5,p6,p4) + (angle p6,p4,p5)) + (angle p4,p5,p6) = PI ) ; :: thesis: angle p2,p3,p1 = angle p6,p4,p5

A12: ( angle p2,p3,p1 < 2 * PI & angle p6,p4,p5 >= 0 ) by COMPLEX2:84;
(angle p2,p3,p1) + (- (angle p6,p4,p5)) < (2 * PI ) + (- 0 ) by A12, XREAL_1:10;
then (4 * PI ) / PI < (2 * PI ) / PI by A5, A11, XREAL_1:76;
then 4 < (2 * PI ) / PI by XCMPLX_1:90;
then 4 < 2 by XCMPLX_1:90;
hence angle p2,p3,p1 = angle p6,p4,p5 ; :: thesis: verum

end;

end;

end;

thus |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| by A1, A2, A3, A4, A5, Lm19; :: thesis: ( |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| )
thus |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| by A2, A3, A4, A5, A8, Lm19; :: thesis: |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).|
thus |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| by A2, A3, A4, A5, A8, Lm19; :: thesis: verum