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

per cases ( ( (angle p1,p,p2) + (angle p2,p,p3) = PI & (angle p2,p,p3) + (angle p3,p,p4) = PI ) or ( (angle p1,p,p2) + (angle p2,p,p3) = 3 * PI & (angle p2,p,p3) + (angle p3,p,p4) = PI ) or ( (angle p1,p,p2) + (angle p2,p,p3) = PI & (angle p2,p,p3) + (angle p3,p,p4) = 3 * PI ) or ( (angle p1,p,p2) + (angle p2,p,p3) = 3 * PI & (angle p2,p,p3) + (angle p3,p,p4) = 3 * PI ) ) by A1, A2, A3, A4, A5, A6, Th13;

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

hence angle p1,p,p2 = angle p3,p,p4 ; :: thesis: verum

end;

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

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

end;

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

angle p3,p,p4 < 2 * PI by COMPLEX2:84;
then (angle p3,p,p4) - (2 * PI ) < (2 * PI ) - (2 * PI ) by XREAL_1:11;
hence angle p1,p,p2 = angle p3,p,p4 by A8, COMPLEX2:84; :: thesis: verum

end;

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

hence angle p1,p,p2 = angle p3,p,p4 ; :: thesis: verum

end;

end;