let p, p1, p3, p2 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg p1,p3 & p <> p1 & p <> p3 & not (angle p1,p,p2) + (angle p2,p,p3) = PI implies (angle p1,p,p2) + (angle p2,p,p3) = 3 * PI )
assume ( p in LSeg p1,p3 & p <> p1 & p <> p3 ) ; :: thesis: ( (angle p1,p,p2) + (angle p2,p,p3) = PI or (angle p1,p,p2) + (angle p2,p,p3) = 3 * PI )
then A1: angle p1,p,p3 = PI by Th8;
( (angle p1,p,p2) + (angle p2,p,p3) = angle p1,p,p3 or (angle p1,p,p2) + (angle p2,p,p3) = (angle p1,p,p3) + (2 * PI ) ) by Th4;
hence ( (angle p1,p,p2) + (angle p2,p,p3) = PI or (angle p1,p,p2) + (angle p2,p,p3) = 3 * PI ) by A1; :: thesis: verum