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

per cases ( angle p1,p2,p3 = 0 or angle p1,p2,p3 <> 0 ) ;

suppose A4: angle p1,p2,p3 = 0 ; :: thesis: angle p1,p2,p3 = angle p1,p2,p

then angle p3,p2,p1 = 0 by EUCLID_3:45;
then A5: angle p,p2,p1 = 0 by A1, A2, Th9;
thus angle p1,p2,p3 = angle p3,p2,p1 by A4, EUCLID_3:45
.= angle p,p2,p1 by A1, A2, Th9
.= angle p1,p2,p by A5, EUCLID_3:45 ; :: thesis: verum

end;

suppose A6: angle p1,p2,p3 <> 0 ; :: thesis: angle p1,p2,p3 = angle p1,p2,p

then A7: angle p,p2,p1 <> 0 by A3, EUCLID_3:45;
thus angle p1,p2,p3 = (2 * PI ) - (angle p3,p2,p1) by A6, EUCLID_3:47
.= (2 * PI ) - (angle p,p2,p1) by A1, A2, Th9
.= angle p1,p2,p by A7, EUCLID_3:46 ; :: thesis: verum

end;

end;