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 A1: 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 A2: p1,p2,p3 are_mutually_distinct by Th20;
then A3: p3 <> p2 by ZFMISC_1:def 5;
A4: angle (p3,p1,p2) <> PI by A1, Th20;
A5: p3 <> p1 by A2, ZFMISC_1:def 5;
then A6: euc2cpx p3 <> euc2cpx p1 by EUCLID_3:4;
A7: p2 <> p1 by A2, ZFMISC_1:def 5;
then A8: euc2cpx p2 <> euc2cpx p1 by EUCLID_3:4;
assume A9: 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 A10: p4,p5,p6 are_mutually_distinct by Th20;
then A11: p4 <> p5 by ZFMISC_1:def 5;
then A12: euc2cpx p4 <> euc2cpx p5 by EUCLID_3:4;
A13: p5 <> p6 by A10, ZFMISC_1:def 5;
then A14: euc2cpx p5 <> euc2cpx p6 by EUCLID_3:4;
A15: angle (p6,p4,p5) <> PI by A9, Th20;
A16: p4 <> p6 by A10, ZFMISC_1:def 5;
then A17: euc2cpx p4 <> euc2cpx p6 by EUCLID_3:4;
assume A18: ( 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).| )
A19: euc2cpx p3 <> euc2cpx p2 by A3, EUCLID_3:4;
A20: 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 A19, A6, A8, A12, A17, A14, COMPLEX2:88;

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 A18; :: 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 A18; :: thesis: verum

end;

suppose A21: ( ((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)

( angle (p2,p3,p1) >= 0 & - (angle (p6,p4,p5)) > - (2 * PI) ) by COMPLEX2:70, XREAL_1:24;
then A22: (angle (p2,p3,p1)) + (- (angle (p6,p4,p5))) > 0 + (- (2 * PI)) by XREAL_1:8;
(angle (p2,p3,p1)) - (angle (p6,p4,p5)) = - (4 * PI) by A18, A21;
then 4 * PI < 2 * PI by A22, XREAL_1:24;
then (4 * PI) / PI < (2 * PI) / PI by XREAL_1:74;
then 4 < (2 * PI) / PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence angle (p2,p3,p1) = angle (p6,p4,p5) ; :: thesis: verum

end;

suppose A23: ( ((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)

( angle (p2,p3,p1) < 2 * PI & angle (p6,p4,p5) >= 0 ) by COMPLEX2:70;
then (angle (p2,p3,p1)) + (- (angle (p6,p4,p5))) < (2 * PI) + (- 0) by XREAL_1:8;
then (4 * PI) / PI < (2 * PI) / PI by A18, A23, XREAL_1:74;
then 4 < (2 * PI) / PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence angle (p2,p3,p1) = angle (p6,p4,p5) ; :: thesis: verum

end;

end;

end;

( angle (p1,p2,p3) <> PI & angle (p2,p3,p1) <> PI ) by A1, Th20;
hence |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| by A4, A3, A5, A7, A15, A11, A16, A13, A18, Lm19; :: thesis: ( |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| & |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| )
A24: ( angle (p4,p5,p6) <> PI & angle (p5,p6,p4) <> PI ) by A9, Th20;
hence |.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| by A3, A5, A7, A15, A11, A16, A13, A18, A20, Lm19; :: thesis: |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).|
thus |.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| by A3, A5, A7, A24, A15, A11, A16, A13, A18, A20, Lm19; :: thesis: verum