let p1, p, p2 be Point of (TOP-REAL 2); :: thesis: ( angle p1,p,p2 = PI implies p in LSeg p1,p2 )
assume A1: angle p1,p,p2 = PI ; :: thesis: p in LSeg p1,p2
set a = p1 `1 ;
set b = p1 `2 ;
A2: p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;
set r = |.(p - p1).|;

per cases ( p = p1 or p = p2 or ( p <> p1 & p <> p2 ) ) ;

suppose ( p = p1 or p = p2 ) ; :: thesis: p in LSeg p1,p2

hence p in LSeg p1,p2 by RLTOPSP1:69; :: thesis: verum

end;

suppose A3: ( p <> p1 & p <> p2 ) ; :: thesis: p in LSeg p1,p2

then A4: |.(p - p1).| <> 0 by Lm1;
|.(p1 - |[(p1 `1 ),(p1 `2 )]|).| = 0 by A2, Lm1;
then |.(p1 - |[(p1 `1 ),(p1 `2 )]|).| < |.(p - p1).| by A4;
then p1 in { p4 where p4 is Point of (TOP-REAL 2) : |.(p4 - |[(p1 `1 ),(p1 `2 )]|).| < |.(p - p1).| } ;
then A5: p1 in inside_of_circle (p1 `1 ),(p1 `2 ),|.(p - p1).| by JGRAPH_6:def 6;
A6: |.(p2 - p1).| ^2 = ((|.(p1 - p).| ^2 ) + (|.(p2 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * (- 1)) by A1, Th7, SIN_COS:82
.= (|.(p1 - p).| + |.(p2 - p).|) ^2 ;
|.(p2 - p1).| > |.(p - p1).|

proof

assume |.(p2 - p1).| <= |.(p - p1).| ; :: thesis: contradiction
then |.(p2 - p1).| ^2 <= |.(p - p1).| ^2 by SQUARE_1:77;
then (|.(p - p1).| + |.(p2 - p).|) ^2 <= |.(p - p1).| ^2 by A6, Lm2;
then (((|.(p - p1).| ^2 ) + ((2 * |.(p - p1).|) * |.(p2 - p).|)) + (|.(p2 - p).| ^2 )) - (|.(p - p1).| ^2 ) <= (|.(p - p1).| ^2 ) - (|.(p - p1).| ^2 ) by XREAL_1:11;
then A7: ((2 * |.(p - p1).|) + |.(p2 - p).|) * |.(p2 - p).| <= 0 ;
|.(p2 - p).| <> 0 by A3, Lm1;
then A8: 0 < |.(p2 - p).| ;
then A9: (2 * |.(p - p1).|) + |.(p2 - p).| <= 0 / |.(p2 - p).| by A7;
(2 * |.(p - p1).|) + |.(p2 - p).| > 0 + 0 by A8;
hence contradiction by A9; :: thesis: verum

end;

then p2 in { p4 where p4 is Point of (TOP-REAL 2) : |.(p4 - |[(p1 `1 ),(p1 `2 )]|).| > |.(p - p1).| } by A2;
then p2 in outside_of_circle (p1 `1 ),(p1 `2 ),|.(p - p1).| by JGRAPH_6:def 8;
then consider p3 being Point of (TOP-REAL 2) such that
A10: p3 in (LSeg p1,p2) /\ (circle (p1 `1 ),(p1 `2 ),|.(p - p1).|) by A5, Lm17;
A11: ( p3 in LSeg p1,p2 & p3 in circle (p1 `1 ),(p1 `2 ),|.(p - p1).| ) by A10, XBOOLE_0:def 4;
then p3 in { p4 where p4 is Point of (TOP-REAL 2) : |.(p4 - |[(p1 `1 ),(p1 `2 )]|).| = |.(p - p1).| } by JGRAPH_6:def 5;
then consider p4 being Point of (TOP-REAL 2) such that
A12: ( p3 = p4 & |.(p4 - |[(p1 `1 ),(p1 `2 )]|).| = |.(p - p1).| ) ;
A13: |.(p3 - p1).| = |.(p - p1).| by A12, EUCLID:57;
|.(p - p1).| <> 0 by A3, Lm1;
then A14: p3 <> p1 by A2, A12, Lm1;
A15: ( euc2cpx p <> euc2cpx p1 & euc2cpx p <> euc2cpx p2 & euc2cpx p1 <> euc2cpx p2 ) by A1, A3, COMPLEX2:93, EUCLID_3:6;
A16: angle p,p1,p2 = 0

proof

assume angle p,p1,p2 <> 0 ; :: thesis: contradiction
then A17: ( angle p,p1,p2 > 0 & angle p,p1,p2 < 2 * PI ) by COMPLEX2:84;

per cases ( ((angle p,p1,p2) + (angle p1,p2,p)) + (angle p2,p,p1) = PI or ((angle p,p1,p2) + (angle p1,p2,p)) + (angle p2,p,p1) = 5 * PI ) by A15, COMPLEX2:102;

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

then A18: ((angle p,p1,p2) + (angle p1,p2,p)) + PI = PI by A1, COMPLEX2:96;
angle p1,p2,p >= 0 by COMPLEX2:84;
then (angle p,p1,p2) + (angle p1,p2,p) > 0 + 0 by A17;
hence contradiction by A18; :: thesis: verum

end;

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

then A19: ((angle p,p1,p2) + (angle p1,p2,p)) + PI = 5 * PI by A1, COMPLEX2:96;
angle p1,p2,p < 2 * PI by COMPLEX2:84;
then (angle p,p1,p2) + (angle p1,p2,p) < (2 * PI ) + (2 * PI ) by A17, XREAL_1:10;
hence contradiction by A19; :: thesis: verum

end;

end;

end;

|.(p3 - p).| ^2 = ((|.(p - p1).| ^2 ) + (|.(p3 - p1).| ^2 )) - (((2 * |.(p - p1).|) * |.(p3 - p1).|) * (cos (angle p,p1,p3))) by Th7
.= ((|.(p - p1).| ^2 ) + (|.(p - p1).| ^2 )) - (((2 * |.(p - p1).|) * |.(p - p1).|) * (cos 0 )) by A11, A13, A14, A16, Th10
.= 0 by SIN_COS:34 ;
then |.(p3 - p).| = 0 ;
hence p in LSeg p1,p2 by A11, Lm1; :: thesis: verum

end;

end;