let p1, p2, p3, p 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:36;
then A5: angle (p,p2,p1) = 0 by A1, A2, Th9;
thus angle (p1,p2,p3) = angle (p3,p2,p1) by A4, EUCLID_3:36
.= angle (p,p2,p1) by A1, A2, Th9
.= angle (p1,p2,p) by A5, EUCLID_3:36 ; :: 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:36;
thus angle (p1,p2,p3) = (2 * PI) - (angle (p3,p2,p1)) by A6, EUCLID_3:38
.= (2 * PI) - (angle (p,p2,p1)) by A1, A2, Th9
.= angle (p1,p2,p) by A7, EUCLID_3:37 ; :: thesis: verum
end;
end;