let p, p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg p1,p2 & p1,p2,p3 is_a_triangle & angle p1,p3,p2 = angle p,p3,p2 implies p = p1 )
assume A1: p in LSeg p1,p2 ; :: thesis: ( not p1,p2,p3 is_a_triangle or not angle p1,p3,p2 = angle p,p3,p2 or p = p1 )
assume A2: p1,p2,p3 is_a_triangle ; :: thesis: ( not angle p1,p3,p2 = angle p,p3,p2 or p = p1 )
then A3: angle p3,p1,p2 <> PI by Th20;
A4: p1,p2,p3 are_mutually_different by A2, Th20;
then p1 <> p2 by ZFMISC_1:def 5;
then A5: euc2cpx p2 <> euc2cpx p1 by EUCLID_3:6;
A6: not p3 in LSeg p1,p2 by A2, Def3;
( not p1 in LSeg p2,p3 & not p2 in LSeg p3,p1 ) by A2, Def3;
then A7: p1,p3,p2 is_a_triangle by A6, Def3;
p2 <> p3 by A4, ZFMISC_1:def 5;
then A8: |.(p2 - p3).| <> 0 by Lm1;
A9: p2 <> p3 by A4, ZFMISC_1:def 5;
then A10: euc2cpx p3 <> euc2cpx p2 by EUCLID_3:6;
assume A11: angle p1,p3,p2 = angle p,p3,p2 ; :: thesis: p = p1
angle p2,p3,p1 <> PI by A2, Th20;
then A12: angle p,p3,p2 <> PI by A11, COMPLEX2:96;
A13: p <> p3 by A1, A2, Def3;
then A14: euc2cpx p <> euc2cpx p3 by EUCLID_3:6;
p1 <> p3 by A4, ZFMISC_1:def 5;
then A15: euc2cpx p3 <> euc2cpx p1 by EUCLID_3:6;
A16: angle p1,p2,p3 <> PI by A2, Th20;
A17: p <> p2

proof

assume p = p2 ; :: thesis: contradiction
then angle p1,p3,p2 = 0 by A11, COMPLEX2:93;
then ( ( angle p3,p2,p1 = 0 & angle p2,p1,p3 = PI ) or ( angle p3,p2,p1 = PI & angle p2,p1,p3 = 0 ) ) by A10, A15, A5, COMPLEX2:101;
hence contradiction by A16, A3, COMPLEX2:96; :: thesis: verum

end;

then A18: angle p3,p2,p1 = angle p3,p2,p by A1, Th10;
then A19: angle p3,p2,p <> PI by A16, COMPLEX2:96;
A20: p,p3,p2 are_mutually_different by A9, A17, A13, ZFMISC_1:def 5;
A21: euc2cpx p <> euc2cpx p2 by A17, EUCLID_3:6;
A22: angle p2,p1,p3 = angle p2,p,p3

proof

per cases ( ( ((angle p1,p3,p2) + (angle p3,p2,p1)) + (angle p2,p1,p3) = PI & ((angle p,p3,p2) + (angle p3,p2,p)) + (angle p2,p,p3) = PI ) or ( ((angle p1,p3,p2) + (angle p3,p2,p1)) + (angle p2,p1,p3) = 5 * PI & ((angle p,p3,p2) + (angle p3,p2,p)) + (angle p2,p,p3) = 5 * PI ) or ( ((angle p1,p3,p2) + (angle p3,p2,p1)) + (angle p2,p1,p3) = PI & ((angle p,p3,p2) + (angle p3,p2,p)) + (angle p2,p,p3) = 5 * PI ) or ( ((angle p1,p3,p2) + (angle p3,p2,p1)) + (angle p2,p1,p3) = 5 * PI & ((angle p,p3,p2) + (angle p3,p2,p)) + (angle p2,p,p3) = PI ) ) by A10, A15, A5, A14, A21, COMPLEX2:102;

suppose ( ((angle p1,p3,p2) + (angle p3,p2,p1)) + (angle p2,p1,p3) = PI & ((angle p,p3,p2) + (angle p3,p2,p)) + (angle p2,p,p3) = PI ) ; :: thesis: angle p2,p1,p3 = angle p2,p,p3

hence angle p2,p1,p3 = angle p2,p,p3 by A11, A18; :: thesis: verum

end;

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

hence angle p2,p1,p3 = angle p2,p,p3 by A11, A18; :: thesis: verum

end;

suppose A23: ( ((angle p1,p3,p2) + (angle p3,p2,p1)) + (angle p2,p1,p3) = PI & ((angle p,p3,p2) + (angle p3,p2,p)) + (angle p2,p,p3) = 5 * PI ) ; :: thesis: angle p2,p1,p3 = angle p2,p,p3

angle p2,p,p3 < 2 * PI by COMPLEX2:84;
then ( angle p2,p1,p3 >= 0 & - (angle p2,p,p3) > - (2 * PI ) ) by COMPLEX2:84, XREAL_1:26;
then A24: (angle p2,p1,p3) + (- (angle p2,p,p3)) > 0 + (- (2 * PI )) by XREAL_1:10;
(angle p2,p1,p3) - (angle p2,p,p3) = - (4 * PI ) by A11, A18, A23;
then 4 * PI < 2 * PI by A24, 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,p1,p3 = angle p2,p,p3 ; :: thesis: verum

end;

suppose A25: ( ((angle p1,p3,p2) + (angle p3,p2,p1)) + (angle p2,p1,p3) = 5 * PI & ((angle p,p3,p2) + (angle p3,p2,p)) + (angle p2,p,p3) = PI ) ; :: thesis: angle p2,p1,p3 = angle p2,p,p3

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

end;

end;

end;

then angle p2,p,p3 <> PI by A3, COMPLEX2:96;
then p,p3,p2 is_a_triangle by A20, A12, A19, Th20;
then |.(p2 - p3).| * |.(p - p2).| = |.(p1 - p2).| * |.(p2 - p3).| by A7, A11, A22, Th21;
then |.(p - p2).| = |.(p1 - p2).| by A8, XCMPLX_1:5;
then A26: |.(p2 - p).| = |.(p1 - p2).| by Lm2
.= |.(p2 - p1).| by Lm2 ;
assume A27: p1 <> p ; :: thesis: contradiction
A28: |.(p2 - p1).| ^2 = ((|.(p1 - p).| ^2 ) + (|.(p2 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * (cos (angle p1,p,p2))) by Th7
.= ((|.(p1 - p).| ^2 ) + (|.(p2 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * (- 1)) by A1, A27, A17, Th8, SIN_COS:82 ;

per cases ( |.(p1 - p).| = 0 or |.(p1 - p).| + (2 * |.(p2 - p).|) = 0 ) by A26, A28;

suppose |.(p1 - p).| = 0 ; :: thesis: contradiction

hence contradiction by A27, Lm1; :: thesis: verum

end;

suppose |.(p1 - p).| + (2 * |.(p2 - p).|) = 0 ; :: thesis: contradiction

then |.(p1 - p).| = 0 ;
hence contradiction by A27, Lm1; :: thesis: verum

end;

end;