let p1, p2, p3, p 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_distinct by A2, Th20;
then p1 <> p2 by ZFMISC_1:def 5;
then A5: euc2cpx p2 <> euc2cpx p1 by EUCLID_3:4;
A6: not p3 in LSeg (p1,p2) by A2, TOPREAL9:67;
( not p1 in LSeg (p2,p3) & not p2 in LSeg (p3,p1) ) by A2, TOPREAL9:67;
then A7: p1,p3,p2 is_a_triangle by A6, TOPREAL9:67;
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:4;
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:82;
A13: p <> p3 by A1, A2, TOPREAL9:67;
then A14: euc2cpx p <> euc2cpx p3 by EUCLID_3:4;
p1 <> p3 by A4, ZFMISC_1:def 5;
then A15: euc2cpx p3 <> euc2cpx p1 by EUCLID_3:4;
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:79;
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:87;
hence contradiction by A16, A3, COMPLEX2:82; :: 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:82;
A20: p,p3,p2 are_mutually_distinct by A9, A17, A13, ZFMISC_1:def 5;
A21: euc2cpx p <> euc2cpx p2 by A17, EUCLID_3:4;
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:88;

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,p1,p3) >= 0 & - (angle (p2,p,p3)) > - (2 * PI) ) by COMPLEX2:70, XREAL_1:24;
then A24: (angle (p2,p1,p3)) + (- (angle (p2,p,p3))) > 0 + (- (2 * PI)) by XREAL_1:8;
(angle (p2,p1,p3)) - (angle (p2,p,p3)) = - (4 * PI) by A11, A18, A23;
then 4 * PI < 2 * PI by A24, 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,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:70;
then (angle (p2,p1,p3)) + (- (angle (p2,p,p3))) < (2 * PI) + (- 0) by XREAL_1:8;
then (4 * PI) / PI < (2 * PI) / PI by A11, A18, A25, XREAL_1:74;
then 4 < (2 * PI) / PI by XCMPLX_1:89;
then 4 < 2 by XCMPLX_1:89;
hence angle (p2,p1,p3) = angle (p2,p,p3) ; :: thesis: verum

end;

end;

end;

then angle (p2,p,p3) <> PI by A3, COMPLEX2:82;
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:77 ;

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;