let p, p2, p3, p1 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg p2,p3 & p <> p2 implies angle p3,p2,p1 = angle p,p2,p1 )
assume p in LSeg p2,p3 ; :: thesis: ( not p <> p2 or angle p3,p2,p1 = angle p,p2,p1 )
then consider l being Real such that
A1: ( p = ((1 - l) * p2) + (l * p3) & 0 <= l & l <= 1 ) ;
A2: p - p2 = (((1 + (- l)) * p2) + (l * p3)) - p2 by A1
.= (((1 * p2) + ((- l) * p2)) + (l * p3)) - p2 by EUCLID:37
.= ((p2 + ((- l) * p2)) + (l * p3)) - p2 by EUCLID:33
.= (p2 + ((- l) * p2)) + ((l * p3) + (- p2)) by EUCLID:30
.= p2 + (((- l) * p2) + ((l * p3) + (- p2))) by EUCLID:30
.= p2 + ((- p2) + (((- l) * p2) + (l * p3))) by EUCLID:30
.= (p2 + (- p2)) + (((- l) * p2) + (l * p3)) by EUCLID:30
.= (0. (TOP-REAL 2)) + (((- l) * p2) + (l * p3)) by EUCLID:40
.= ((l * (- 1)) * p2) + (l * p3) by EUCLID:31
.= (l * ((- 1) * p2)) + (l * p3) by EUCLID:34
.= (l * (- p2)) + (l * p3) by EUCLID:43
.= l * (p3 - p2) by EUCLID:36 ;
assume A3: p <> p2 ; :: thesis: angle p3,p2,p1 = angle p,p2,p1
set c = euc2cpx (p - p2);
set c1 = euc2cpx (p1 - p2);
set c3 = euc2cpx (p3 - p2);
A4: l <> 0

proof

assume l = 0 ; :: thesis: contradiction
then p = (1 * p2) + (0. (TOP-REAL 2)) by A1, EUCLID:33
.= 1 * p2 by EUCLID:31
.= p2 by EUCLID:33 ;
hence contradiction by A3; :: thesis: verum

end;

cpx2euc ((euc2cpx (p3 - p2)) * l) = l * (cpx2euc (euc2cpx (p3 - p2))) by EUCLID_3:23
.= l * (p3 - p2) by EUCLID_3:2
.= cpx2euc (euc2cpx (p - p2)) by A2, EUCLID_3:2 ;
then euc2cpx (p - p2) = (euc2cpx (p3 - p2)) * l by EUCLID_3:5;
then A5: Arg (euc2cpx (p - p2)) = Arg (euc2cpx (p3 - p2)) by A1, A4, COMPLEX2:40;
angle (euc2cpx (p3 - p2)),(euc2cpx (p1 - p2)) = angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2))

proof

per cases ( Arg (euc2cpx (p3 - p2)) = 0 or euc2cpx (p1 - p2) <> 0 or ( not Arg (euc2cpx (p3 - p2)) = 0 & not euc2cpx (p1 - p2) <> 0 ) ) ;

suppose A6: ( Arg (euc2cpx (p3 - p2)) = 0 or euc2cpx (p1 - p2) <> 0 ) ; :: thesis: angle (euc2cpx (p3 - p2)),(euc2cpx (p1 - p2)) = angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2))

then angle (euc2cpx (p3 - p2)),(euc2cpx (p1 - p2)) = Arg (Rotate (euc2cpx (p1 - p2)),(- (Arg (euc2cpx (p3 - p2))))) by COMPLEX2:def 5
.= angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2)) by A5, A6, COMPLEX2:def 5 ;
hence angle (euc2cpx (p3 - p2)),(euc2cpx (p1 - p2)) = angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2)) ; :: thesis: verum

end;

suppose A7: ( not Arg (euc2cpx (p3 - p2)) = 0 & not euc2cpx (p1 - p2) <> 0 ) ; :: thesis: angle (euc2cpx (p3 - p2)),(euc2cpx (p1 - p2)) = angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2))

then angle (euc2cpx (p3 - p2)),(euc2cpx (p1 - p2)) = (2 * PI ) - (Arg (euc2cpx (p3 - p2))) by COMPLEX2:def 5
.= angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2)) by A5, A7, COMPLEX2:def 5 ;
hence angle (euc2cpx (p3 - p2)),(euc2cpx (p1 - p2)) = angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2)) ; :: thesis: verum

end;

end;

end;

hence angle p3,p2,p1 = angle (euc2cpx (p - p2)),(euc2cpx (p1 - p2)) by Lm7
.= angle p,p2,p1 by Lm7 ;
:: thesis: verum