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

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

end;

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

A18: ( angle p1,p3,p2 >= 0 & angle p2,p1,p3 >= 0 ) by COMPLEX2:84;
angle p2,p,p3 < 2 * PI by COMPLEX2:84;
then A19: - (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 A19, 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 A18, XREAL_1:10;
hence (angle p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3) by A10, A17; :: thesis: verum

end;

suppose A20: ( ((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 A21: (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 A21, XREAL_1:10;
hence (angle p1,p3,p2) + (angle p2,p1,p3) = (angle p,p3,p2) + (angle p2,p,p3) by A10, A20; :: thesis: verum

end;

end;

end;

then angle p2,p1,p3 < angle p2,p,p3 by A5, XREAL_1:10;
then A22: 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, A4, A14, A12, A11, Th13, COMPLEX2:102;

suppose A23: ( (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, A13, A15, ZFMISC_1:def 5;
then angle p2,p1,p3 > PI by A3, Th24;
then A24: angle p,p1,p3 > PI by A1, A7, Th9;
p,p1,p3 are_mutually_different by A1, A2, A7, A13, ZFMISC_1:def 5;
then ( angle p1,p3,p > PI & angle p3,p,p1 > PI ) by A24, Th24;
then (angle p3,p,p1) + (angle p1,p3,p) > PI + PI by XREAL_1:10;
then A25: ((angle p3,p,p1) + (angle p1,p3,p)) + (angle p,p1,p3) > (2 * PI ) + PI by A24, XREAL_1:10;
1 * PI < 3 * PI by XREAL_1:70;
hence contradiction by A23, A25; :: thesis: verum

end;

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

A27: ( 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 A26;
then angle p2,p,p3 >= 0 + (2 * PI ) by A27, XREAL_1:8;
hence contradiction by COMPLEX2:84; :: thesis: verum

end;

suppose A28: ( (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 A28;
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 A22, 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;