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

proof

assume A4: angle (p1,p3,p) = angle (p,p3,p2) ; :: thesis: |.(p1 - p).| = |.(p - p2).|
A5: |.(p - p1).| ^2 = ((|.(p1 - p3).| ^2) + (|.(p - p3).| ^2)) - (((2 * |.(p1 - p3).|) * |.(p - p3).|) * (cos (angle (p1,p3,p)))) by Th7
.= ((|.(p - p3).| ^2) + (|.(p2 - p3).| ^2)) - (((2 * |.(p - p3).|) * |.(p2 - p3).|) * (cos (angle (p,p3,p2)))) by A1, A4
.= |.(p2 - p).| ^2 by Th7 ;
thus |.(p1 - p).| = |.(p - p1).| by Lm2
.= sqrt (|.(p2 - p).| ^2) by A5, SQUARE_1:22
.= |.(p2 - p).| by SQUARE_1:22
.= |.(p - p2).| by Lm2 ; :: thesis: verum

end;

thus ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p),(p2 - p1))| = 0 ) :: thesis: ( |((p3 - p),(p2 - p1))| = 0 implies angle (p1,p3,p) = angle (p,p3,p2) )

proof

assume A6: |.(p1 - p).| = |.(p - p2).| ; :: thesis: |((p3 - p),(p2 - p1))| = 0

per cases ( p = p2 or p <> p2 ) ;

suppose A7: p = p2 ; :: thesis: |((p3 - p),(p2 - p1))| = 0

then |.(p1 - p).| = 0 by A6, Lm1;
hence |((p3 - p),(p2 - p1))| = |((p3 - p),(p - p))| by A7, Lm1
.= |((p3 - p),(0. (TOP-REAL 2)))| by RLVECT_1:5
.= 0 by EUCLID_2:32 ;
:: thesis: verum

end;

suppose A8: p <> p2 ; :: thesis: |((p3 - p),(p2 - p1))| = 0

then |.(p1 - p).| <> 0 by A6, Lm1;
then A9: p <> p1 by Lm1;
A10: cos (angle (p1,p,p3)) = - (cos (angle (p3,p,p2)))

proof

per cases ( (angle (p1,p,p3)) + (angle (p3,p,p2)) = PI or (angle (p1,p,p3)) + (angle (p3,p,p2)) = 3 * PI ) by A2, A8, A9, Th13;

suppose (angle (p1,p,p3)) + (angle (p3,p,p2)) = PI ; :: thesis: cos (angle (p1,p,p3)) = - (cos (angle (p3,p,p2)))

hence cos (angle (p1,p,p3)) = cos (PI + (- (angle (p3,p,p2))))
.= - (cos (- (angle (p3,p,p2)))) by SIN_COS:79
.= - (cos (angle (p3,p,p2))) by SIN_COS:31 ;
:: thesis: verum

end;

suppose (angle (p1,p,p3)) + (angle (p3,p,p2)) = 3 * PI ; :: thesis: cos (angle (p1,p,p3)) = - (cos (angle (p3,p,p2)))

hence cos (angle (p1,p,p3)) = cos ((PI - (angle (p3,p,p2))) + (2 * PI))
.= cos (PI + (- (angle (p3,p,p2)))) by SIN_COS:79
.= - (cos (- (angle (p3,p,p2)))) by SIN_COS:79
.= - (cos (angle (p3,p,p2))) by SIN_COS:31 ;
:: thesis: verum

end;

end;

end;

A11: ( |.(p3 - p1).| ^2 = ((|.(p1 - p).| ^2) + (|.(p3 - p).| ^2)) - (((2 * |.(p1 - p).|) * |.(p3 - p).|) * (cos (angle (p1,p,p3)))) & |.(p2 - p3).| ^2 = ((|.(p3 - p).| ^2) + (|.(p2 - p).| ^2)) - (((2 * |.(p3 - p).|) * |.(p2 - p).|) * (cos (angle (p3,p,p2)))) ) by Th7;
A12: |.(p1 - p).| = |.(p2 - p).| by A6, Lm2;
A13: |.(p2 - p).| <> 0 by A8, Lm1;
A14: |.(p3 - p).| <> 0 by A3, Lm1;
|.(p3 - p1).| = |.(p2 - p3).| by A1, Lm2;
then ((2 * |.(p1 - p).|) * (cos (angle (p1,p,p3)))) * |.(p3 - p).| = ((2 * |.(p2 - p).|) * (cos (angle (p3,p,p2)))) * |.(p3 - p).| by A11, A12;
then (2 * (cos (angle (p1,p,p3)))) * |.(p2 - p).| = (2 * (cos (angle (p3,p,p2)))) * |.(p2 - p).| by A14, A12, XCMPLX_1:5;
then A15: 2 * (cos (angle (p1,p,p3))) = 2 * (cos (angle (p3,p,p2))) by A13, XCMPLX_1:5;
( 0 <= angle (p3,p,p2) & angle (p3,p,p2) < 2 * PI ) by COMPLEX2:70;
then ( angle (p3,p,p2) = PI / 2 or angle (p3,p,p2) = (3 / 2) * PI ) by A15, A10, COMPTRIG:18;
then |((p3 - p),(p2 - p))| = 0 by A3, A8, EUCLID_3:45;
hence |((p3 - p),(p2 - p1))| = 0 by A2, A8, Th17; :: thesis: verum

end;

end;

end;

thus ( |((p3 - p),(p2 - p1))| = 0 implies angle (p1,p3,p) = angle (p,p3,p2) ) :: thesis: verum

proof

assume A16: |((p3 - p),(p2 - p1))| = 0 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
then A17: 0 = - |((p3 - p),(p2 - p1))|
.= |((p3 - p),(- (p2 - p1)))| by EUCLID_2:22
.= |((p3 - p),(p1 - p2))| by RLVECT_1:33 ;

per cases ( ( p2 = p & p1 = p ) or p1 <> p or p2 <> p ) ;

suppose ( p2 = p & p1 = p ) ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)

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

end;

suppose A18: p1 <> p ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)

then |((p3 - p),(p1 - p))| = 0 by A2, A17, Th17;
then ( angle (p3,p,p1) = PI / 2 or angle (p3,p,p1) = (3 / 2) * PI ) by A3, A18, EUCLID_3:45;
hence angle (p1,p3,p) = angle (p,p3,p2) by A1, A2, A3, A18, Th18; :: thesis: verum

end;

suppose A19: p2 <> p ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)

then |((p3 - p),(p2 - p))| = 0 by A2, A16, Th17;
then ( angle (p3,p,p2) = PI / 2 or angle (p3,p,p2) = (3 / 2) * PI ) by A3, A19, EUCLID_3:45;
then A20: angle (p2,p3,p) = angle (p,p3,p1) by A1, A2, A3, A19, Th18;

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

suppose A21: angle (p2,p3,p) = 0 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)

then angle (p,p3,p2) = 0 by EUCLID_3:36;
hence angle (p1,p3,p) = angle (p,p3,p2) by A20, A21, EUCLID_3:36; :: thesis: verum

end;

suppose A22: angle (p2,p3,p) <> 0 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)

then angle (p,p3,p2) = (2 * PI) - (angle (p2,p3,p)) by EUCLID_3:37;
hence angle (p1,p3,p) = angle (p,p3,p2) by A20, A22, EUCLID_3:37; :: thesis: verum

end;

end;

end;

end;

end;