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

proof

per cases ( ( (angle p2,p,p3) + (angle p3,p,p1) = PI & angle p3,p,p1 = PI / 2 ) or ( (angle p2,p,p3) + (angle p3,p,p1) = 3 * PI & angle p3,p,p1 = (3 / 2) * PI ) or ( (angle p2,p,p3) + (angle p3,p,p1) = PI & angle p3,p,p1 = (3 / 2) * PI ) or ( (angle p2,p,p3) + (angle p3,p,p1) = 3 * PI & angle p3,p,p1 = PI / 2 ) ) by A1, A2, Th13;

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

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

end;

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

(- PI ) / 2 < 0 / 2 ;
hence angle p3,p,p1 = angle p2,p,p3 by A4, COMPLEX2:84; :: thesis: verum

end;

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

0 + (2 * PI ) < (PI / 2) + (2 * PI ) by XREAL_1:8;
hence angle p3,p,p1 = angle p2,p,p3 by A5, COMPLEX2:84; :: thesis: verum

end;

end;

end;

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

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

then angle p1,p,p3 = 0 by EUCLID_3:45;
hence angle p1,p,p3 = angle p3,p,p2 by A3, A6, EUCLID_3:45; :: thesis: verum

end;

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

then angle p1,p,p3 = (2 * PI ) - (angle p3,p,p1) by EUCLID_3:46;
hence angle p1,p,p3 = angle p3,p,p2 by A3, A7, EUCLID_3:46; :: thesis: verum

end;

end;