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

proof

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

end;

l <> 1

proof

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

end;

then l < 1 by A1, XXREAL_0:1;
then - 1 < - l by XREAL_1:26;
then A7: (- 1) + 1 < (- l) + 1 by XREAL_1:8;
then 0 / (1 - l) < l / (1 - l) by A1, A6;
then A8: - (l / (1 - l)) < - 0 ;
cpx2euc ((euc2cpx (p2 - p)) * (- (l / (1 - l)))) = (- (l / (1 - l))) * (cpx2euc (euc2cpx (p2 - p))) by EUCLID_3:23
.= (- (l / (1 - l))) * ((1 - l) * ((- p1) + p2)) by A5, EUCLID_3:2
.= ((- (l / (1 - l))) * (1 - l)) * ((- p1) + p2) by EUCLID:34
.= (((- l) / (1 - l)) * (1 - l)) * ((- p1) + p2) by XCMPLX_1:188
.= (((1 - l) / (1 - l)) * (- l)) * ((- p1) + p2) by XCMPLX_1:76
.= (1 * (- l)) * ((- p1) + p2) by A7, XCMPLX_1:60
.= (l * (- 1)) * ((- p1) + p2)
.= l * ((- 1) * ((- p1) + p2)) by EUCLID:34
.= l * (((- 1) * (- p1)) + ((- 1) * p2)) by EUCLID:36
.= l * ((- (- p1)) + ((- 1) * p2)) by EUCLID:43
.= l * ((- (- p1)) + (- p2)) by EUCLID:43
.= l * ((- (- p1)) + (- p2))
.= l * (p1 + (- p2)) by EUCLID:39
.= cpx2euc (euc2cpx (p1 - p)) by A4, EUCLID_3:2 ;
then euc2cpx (p1 - p) = (euc2cpx (p2 - p)) * (- (l / (1 - l))) by EUCLID_3:5;
then A9: Arg (- (euc2cpx (p2 - p))) = Arg (euc2cpx (p1 - p)) by A8, COMPLEX2:41;
A10: - (euc2cpx (p2 - p)) <> 0

proof

assume - (euc2cpx (p2 - p)) = 0 ; :: thesis: contradiction
then |.(p2 - p).| = 0 by COMPLEX1:130, EUCLID_3:31;
then p2 - p = 0. (TOP-REAL 2) by EUCLID_2:64;
hence contradiction by A3, EUCLID:47; :: thesis: verum

end;

angle (euc2cpx (p1 - p)),(- (euc2cpx (p2 - p))) = 0

proof

per cases ( (Arg (- (euc2cpx (p2 - p)))) - (Arg (euc2cpx (p1 - p))) < 0 or (Arg (- (euc2cpx (p2 - p)))) - (Arg (euc2cpx (p1 - p))) >= 0 ) ;

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

hence angle (euc2cpx (p1 - p)),(- (euc2cpx (p2 - p))) = 0 by A9; :: thesis: verum

end;

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

hence angle (euc2cpx (p1 - p)),(- (euc2cpx (p2 - p))) = 0 by A9, A10, Lm11; :: thesis: verum

end;

end;

end;

then angle (euc2cpx (p1 - p)),(- (- (euc2cpx (p2 - p)))) = PI by A10, COMPLEX2:82;
hence angle p1,p,p2 = PI by Lm7; :: thesis: verum