let p1, p2, p3, p4, p 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:70;
then (angle (p3,p,p4)) + (2 * PI) >= 0 + (2 * PI) by XREAL_1:6;
hence angle (p1,p,p2) = angle (p3,p,p4) by A7, COMPLEX2:70; :: 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:70;
then (angle (p3,p,p4)) - (2 * PI) < (2 * PI) - (2 * PI) by XREAL_1:9;
hence angle (p1,p,p2) = angle (p3,p,p4) by A8, COMPLEX2:70; :: 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;