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 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 angle p,p3,p2 <= angle p1,p3,p2 )
assume A2: not p3 in LSeg p1,p2 ; :: thesis: ( not angle p1,p3,p2 <= PI or angle p,p3,p2 <= angle p1,p3,p2 )
assume A3: angle p1,p3,p2 <= PI ; :: thesis: angle p,p3,p2 <= angle p1,p3,p2
assume A4: angle p,p3,p2 > angle p1,p3,p2 ; :: thesis: contradiction

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

suppose p = p1 ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose p = p2 ; :: thesis: contradiction

then angle p,p3,p2 = 0 by COMPLEX2:93;
hence contradiction by A4, COMPLEX2:84; :: thesis: verum

end;

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

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

end;

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

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

end;

suppose A15: ( ((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)

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

end;

suppose A18: ( ((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)

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

end;

end;

end;

then A20: angle p2,p1,p3 > angle p2,p,p3 by A4, XREAL_1:10;

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, A6, A9, A11, A7, Th13, COMPLEX2:102;

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

then (angle p1,p3,p) + (angle p,p1,p3) < 0 + (angle p,p1,p3) by A1, A20, Th9;
then angle p1,p3,p < 0 by XREAL_1:8;
hence contradiction by COMPLEX2:84; :: thesis: verum

end;

suppose A21: ( (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

A22: ( angle p,p1,p3 >= 0 & angle p1,p3,p >= 0 ) by COMPLEX2:84;
angle p2,p,p3 = ((angle p,p1,p3) + (angle p1,p3,p)) + (2 * PI ) by A21;
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 A24: ( (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

p1,p3,p2 are_mutually_different by A6, A8, A13, ZFMISC_1:def 5;
then angle p2,p1,p3 <= PI by A3, Th23;
then A25: angle p,p1,p3 <= PI by A1, A6, Th9;
p,p1,p3 are_mutually_different by A1, A2, A6, A8, ZFMISC_1:def 5;
then ( angle p1,p3,p <= PI & angle p3,p,p1 <= PI ) by A25, Th23;
then (angle p3,p,p1) + (angle p1,p3,p) <= PI + PI by XREAL_1:9;
then ((angle p3,p,p1) + (angle p1,p3,p)) + (angle p,p1,p3) <= (2 * PI ) + PI by A25, XREAL_1:9;
hence contradiction by A24, XREAL_1:70; :: thesis: verum

end;

end;

end;

end;