let p1, p2, p3, p 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:79;
hence contradiction by A4, COMPLEX2:70; :: thesis: verum

end;

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

then p in {p2} by A1, RLTOPSP1:70;
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:4;
A8: p3 <> p1 by A2, RLTOPSP1:68;
then A9: euc2cpx p3 <> euc2cpx p1 by EUCLID_3:4;
A10: ( euc2cpx p2 <> euc2cpx p1 & euc2cpx p <> euc2cpx p2 ) by A6, EUCLID_3:4;
A11: euc2cpx p <> euc2cpx p3 by A1, A2, EUCLID_3:4;
A12: angle (p3,p2,p1) = angle (p3,p2,p) by A1, A6, Th10;
A13: p3 <> p2 by A2, RLTOPSP1:68;
then A14: euc2cpx p3 <> euc2cpx p2 by EUCLID_3:4;
(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:88;

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:70;
angle (p2,p,p3) < 2 * PI by COMPLEX2:70;
then A17: - (angle (p2,p,p3)) > - (2 * PI) by XREAL_1:24;
angle (p,p3,p2) < 2 * PI by COMPLEX2:70;
then - (angle (p,p3,p2)) > - (2 * PI) by XREAL_1:24;
then (- (angle (p,p3,p2))) + (- (angle (p2,p,p3))) > (- (2 * PI)) + (- (2 * PI)) by A17, XREAL_1:8;
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:8;
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:70;
then A19: (angle (p2,p1,p3)) + (angle (p1,p3,p2)) < (2 * PI) + (2 * PI) by XREAL_1:8;
( angle (p,p3,p2) >= 0 & angle (p2,p,p3) >= 0 ) by COMPLEX2:70;
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:8;
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:8;

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:88;

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:6;
hence contradiction by COMPLEX2:70; :: 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:70;
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:6;
hence contradiction by COMPLEX2:70; :: 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:70;
then (angle (p,p1,p3)) + (angle (p1,p3,p)) < (2 * PI) + (2 * PI) by XREAL_1:8;
then (angle (p2,p,p3)) + (4 * PI) < 0 + (4 * PI) by A23;
then angle (p2,p,p3) < 0 by XREAL_1:6;
hence contradiction by COMPLEX2:70; :: 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_distinct 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_distinct 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:7;
then ((angle (p3,p,p1)) + (angle (p1,p3,p))) + (angle (p,p1,p3)) <= (2 * PI) + PI by A25, XREAL_1:7;
hence contradiction by A24, XREAL_1:68; :: thesis: verum

end;

end;

end;

end;