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 r = |.(p - p1).|;
set b = p1 `2 ;
set a = p1 `1 ;
A2: p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;

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

A4: |.(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 A4, 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 A5: ((2 * |.(p - p1).|) + |.(p2 - p).|) * |.(p2 - p).| <= 0 ;
|.(p2 - p).| <> 0 by A3, Lm1;
hence contradiction by A5; :: 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 A6: p2 in outside_of_circle (p1 `1 ),(p1 `2 ),|.(p - p1).| by JGRAPH_6:def 8;
A7: |.(p1 - |[(p1 `1 ),(p1 `2 )]|).| = 0 by A2, Lm1;
|.(p - p1).| <> 0 by A3, Lm1;
then p1 in { p4 where p4 is Point of (TOP-REAL 2) : |.(p4 - |[(p1 `1 ),(p1 `2 )]|).| < |.(p - p1).| } by A7;
then p1 in inside_of_circle (p1 `1 ),(p1 `2 ),|.(p - p1).| by JGRAPH_6:def 6;
then consider p3 being Point of (TOP-REAL 2) such that
A8: p3 in (LSeg p1,p2) /\ (circle (p1 `1 ),(p1 `2 ),|.(p - p1).|) by A6, Lm17;
A9: euc2cpx p1 <> euc2cpx p2 by A1, COMPLEX2:93;
A10: ( euc2cpx p <> euc2cpx p1 & euc2cpx p <> euc2cpx p2 ) by A3, EUCLID_3:6;
A11: angle p,p1,p2 = 0

proof

assume angle p,p1,p2 <> 0 ; :: thesis: contradiction
then A12: angle p,p1,p2 > 0 by COMPLEX2:84;
A13: 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 A10, A9, COMPLEX2:102;

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

A15: angle p1,p2,p >= 0 by COMPLEX2:84;
((angle p,p1,p2) + (angle p1,p2,p)) + PI = PI by A1, A14, COMPLEX2:96;
hence contradiction by A12, A15; :: thesis: verum

end;

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

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

end;

end;

end;

p3 in circle (p1 `1 ),(p1 `2 ),|.(p - p1).| by A8, 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 A18: ex p4 being Point of (TOP-REAL 2) st
( p3 = p4 & |.(p4 - |[(p1 `1 ),(p1 `2 )]|).| = |.(p - p1).| ) ;
then A19: |.(p3 - p1).| = |.(p - p1).| by EUCLID:57;
|.(p - p1).| <> 0 by A3, Lm1;
then A20: p3 <> p1 by A2, A18, Lm1;
A21: p3 in LSeg p1,p2 by A8, XBOOLE_0:def 4;
|.(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 A21, A19, A20, A11, Th10
.= 0 by SIN_COS:34 ;
then |.(p3 - p).| = 0 ;
hence p in LSeg p1,p2 by A21, Lm1; :: thesis: verum

end;

end;