let p1, p2, p3, p 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:70; :: 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:6;
hence angle (p3,p,p1) = angle (p2,p,p3) by A5, COMPLEX2:70; :: 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:36;
hence angle (p1,p,p3) = angle (p3,p,p2) by A3, A6, EUCLID_3:36; :: 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:37;
hence angle (p1,p,p3) = angle (p3,p,p2) by A3, A7, EUCLID_3:37; :: thesis: verum
end;
end;