let p, p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg p1,p2 & not p3 in LSeg p1,p2 & angle p1,p3,p2 > PI & p <> p2 implies angle p,p3,p2 >= angle p1,p3,p2 )
assume A1: p in LSeg p1,p2 ; :: thesis: ( p3 in LSeg p1,p2 or not angle p1,p3,p2 > PI or not p <> p2 or angle p,p3,p2 >= angle p1,p3,p2 )
assume A2: not p3 in LSeg p1,p2 ; :: thesis: ( not angle p1,p3,p2 > PI or not p <> p2 or angle p,p3,p2 >= angle p1,p3,p2 )
assume A3: angle p1,p3,p2 > PI ; :: thesis: ( not p <> p2 or angle p,p3,p2 >= angle p1,p3,p2 )
assume A4: p <> p2 ; :: thesis: angle p,p3,p2 >= angle p1,p3,p2
assume A5: angle p,p3,p2 < angle p1,p3,p2 ; :: thesis: contradiction

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

suppose p = p1 ; :: thesis: contradiction

hence contradiction by A5; :: thesis: verum

end;

suppose A6: p1 = p2 ; :: thesis: contradiction

then p in {p2} by A1, RLTOPSP1:71;
hence contradiction by A5, A6, TARSKI:def 1; :: thesis: verum

end;

suppose A7: ( p1 <> p2 & p <> p1 ) ; :: thesis: contradiction

A8: ( p3 <> p1 & p3 <> p2 ) by A2, RLTOPSP1:69;
then A9: ( euc2cpx p3 <> euc2cpx p2 & euc2cpx p3 <> euc2cpx p1 & euc2cpx p2 <> euc2cpx p1 ) by A7, EUCLID_3:6;
A10: ( euc2cpx p <> euc2cpx p3 & euc2cpx p <> euc2cpx p2 & euc2cpx p <> euc2cpx p1 ) by A1, A2, A4, A7, EUCLID_3:6;
A11: angle p3,p2,p1 = angle p3,p2,p by A1, A4, Th10;
(angle p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (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 A9, A10, 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 p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3)

hence (angle p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3) by A11; :: 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 p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3)

hence (angle p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3) by A11; :: thesis: verum

end;

suppose A12: ( ((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 p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3)

A13: ( angle p1,p3,p2 >= 0 & angle p2,p1,p3 >= 0 & angle p,p3,p2 < 2 * PI & angle p2,p,p3 < 2 * PI ) by COMPLEX2:84;
then ( - (angle p2,p,p3) > - (2 * PI ) & - (angle p,p3,p2) > - (2 * PI ) ) by XREAL_1:26;
then A14: (- (angle p,p3,p2)) + (- (angle p2,p,p3)) > (- (2 * PI )) + (- (2 * PI )) by XREAL_1:10;
(angle p1,p3,p2) + (angle p2,p1,p3) >= 0 + 0 by A13;
then ((angle p1,p3,p2) + (angle p2,p1,p3)) + ((- (angle p,p3,p2)) - (angle p2,p,p3)) > (0 + 0 ) + ((- (2 * PI )) - (2 * PI )) by A14, XREAL_1:10;
hence (angle p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3) by A11, A12; :: thesis: verum

end;

suppose A15: ( ((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 p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3)

A16: ( angle p2,p1,p3 < 2 * PI & angle p1,p3,p2 < 2 * PI & angle p,p3,p2 >= 0 & angle p2,p,p3 >= 0 ) by COMPLEX2:84;
then A17: (angle p2,p1,p3) + (angle p1,p3,p2) < (2 * PI ) + (2 * PI ) by XREAL_1:10;
( - (angle p2,p,p3) <= - 0 & - (angle p,p3,p2) <= - 0 ) by A16;
then (- (angle p,p3,p2)) + (- (angle p2,p,p3)) <= 0 + 0 ;
then ((angle p2,p1,p3) + (angle p1,p3,p2)) + ((- (angle p,p3,p2)) - (angle p2,p,p3)) < ((2 * PI ) + (2 * PI )) + (0 + 0 ) by A17, XREAL_1:10;
hence (angle p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3) by A11, A15; :: thesis: verum

end;

end;

end;

then angle p2,p1,p3 < angle p2,p,p3 by A5, XREAL_1:10;
then A18: angle p,p1,p3 < angle p2,p,p3 by A1, Th9;

per cases ( ( (angle p2,p,p3) + (angle p3,p,p1) = PI & ((angle p3,p,p1) + (angle p,p1,p3)) + (angle p1,p3,p) = PI ) or ( (angle p2,p,p3) + (angle p3,p,p1) = 3 * PI & ((angle p3,p,p1) + (angle p,p1,p3)) + (angle p1,p3,p) = PI ) or ( (angle p2,p,p3) + (angle p3,p,p1) = PI & ((angle p3,p,p1) + (angle p,p1,p3)) + (angle p1,p3,p) = 5 * PI ) or ( (angle p2,p,p3) + (angle p3,p,p1) = 3 * PI & ((angle p3,p,p1) + (angle p,p1,p3)) + (angle p1,p3,p) = 5 * PI ) ) by A1, A9, A10, Th13, COMPLEX2:102;

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

p1,p3,p2 are_mutually_different by A7, A8, ZFMISC_1:def 5;
then angle p2,p1,p3 > PI by A3, Th24;
then A20: angle p,p1,p3 > PI by A1, A7, Th9;
p,p1,p3 are_mutually_different by A1, A2, A7, A8, ZFMISC_1:def 5;
then ( angle p1,p3,p > PI & angle p3,p,p1 > PI ) by A20, Th24;
then (angle p3,p,p1) + (angle p1,p3,p) > PI + PI by XREAL_1:10;
then A21: ((angle p3,p,p1) + (angle p1,p3,p)) + (angle p,p1,p3) > (2 * PI ) + PI by A20, XREAL_1:10;
1 * PI < 3 * PI by XREAL_1:70;
hence contradiction by A19, A21; :: thesis: verum

end;

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

then A22: angle p2,p,p3 = ((angle p,p1,p3) + (angle p1,p3,p)) + (2 * PI ) ;
( angle p,p1,p3 >= 0 & angle p1,p3,p >= 0 ) by COMPLEX2:84;
then (angle p,p1,p3) + (angle p1,p3,p) >= 0 + 0 ;
then angle p2,p,p3 >= 0 + (2 * PI ) by A22, XREAL_1:8;
hence contradiction by COMPLEX2:84; :: thesis: verum

end;

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

( angle p,p1,p3 < 2 * PI & angle p1,p3,p < 2 * PI ) by COMPLEX2:84;
then (angle p,p1,p3) + (angle p1,p3,p) < (2 * PI ) + (2 * PI ) by XREAL_1:10;
then (angle p2,p,p3) + (4 * PI ) < 0 + (4 * PI ) by A23;
then angle p2,p,p3 < 0 by XREAL_1:8;
hence contradiction by COMPLEX2:84; :: thesis: verum

end;

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

then (angle p2,p,p3) + (2 * PI ) = (angle p,p1,p3) + (angle p1,p3,p) ;
then (angle p2,p,p3) + (2 * PI ) < (angle p2,p,p3) + (angle p1,p3,p) by A18, XREAL_1:8;
then 2 * PI < angle p1,p3,p by XREAL_1:8;
hence contradiction by COMPLEX2:84; :: thesis: verum

end;

end;

end;

end;