let p1, p2, p3, p 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