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

per cases ( p1,p2,p3 are_mutually_different or not p1,p2,p3 are_mutually_different ) ;

suppose A3: p1,p2,p3 are_mutually_different ; :: thesis: angle p3,p1,p2 = angle p1,p2,p3

|.(p3 - p1).| ^2 = ((|.(p1 - p2).| ^2 ) + (|.(p3 - p2).| ^2 )) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle p1,p2,p3))) by Th7;
then ((|.(p1 - p2).| ^2 ) + (|.(p3 - p2).| ^2 )) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle p1,p2,p3))) = ((|.(p3 - p1).| ^2 ) + (|.(p2 - p1).| ^2 )) - (((2 * |.(p3 - p1).|) * |.(p2 - p1).|) * (cos (angle p3,p1,p2))) by A1, Th7;
then ((|.(p3 - p2).| ^2 ) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle p1,p2,p3)))) + (|.(p1 - p2).| ^2 ) = ((|.(p3 - p1).| ^2 ) - (((2 * |.(p3 - p1).|) * |.(p2 - p1).|) * (cos (angle p3,p1,p2)))) + (|.(p2 - p1).| ^2 ) ;
then ((|.(p3 - p2).| ^2 ) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle p1,p2,p3)))) + (|.(p1 - p2).| ^2 ) = ((|.(p3 - p1).| ^2 ) - (((2 * |.(p3 - p1).|) * |.(p2 - p1).|) * (cos (angle p3,p1,p2)))) + (|.(p1 - p2).| ^2 ) by Lm2;
then (- (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle p1,p2,p3)))) + (|.(p3 - p2).| ^2 ) = (- (((2 * |.(p2 - p3).|) * |.(p2 - p1).|) * (cos (angle p3,p1,p2)))) + (|.(p2 - p3).| ^2 ) by A1;
then (- (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle p1,p2,p3)))) + (|.(p3 - p2).| ^2 ) = (- (((2 * |.(p2 - p3).|) * |.(p2 - p1).|) * (cos (angle p3,p1,p2)))) + (|.(p3 - p2).| ^2 ) by Lm2;
then (|.(p1 - p2).| * |.(p3 - p2).|) * (cos (angle p1,p2,p3)) = (|.(p2 - p3).| * |.(p2 - p1).|) * (cos (angle p3,p1,p2)) ;
then (|.(p1 - p2).| * |.(p3 - p2).|) * (cos (angle p1,p2,p3)) = (|.(p2 - p3).| * |.(p1 - p2).|) * (cos (angle p3,p1,p2)) by Lm2;
then A4: (|.(p3 - p2).| * (cos (angle p1,p2,p3))) * |.(p1 - p2).| = (|.(p2 - p3).| * (cos (angle p3,p1,p2))) * |.(p1 - p2).| ;
p1 <> p2 by A3, ZFMISC_1:def 5;
then |.(p1 - p2).| <> 0 by Lm1;
then |.(p3 - p2).| * (cos (angle p1,p2,p3)) = |.(p2 - p3).| * (cos (angle p3,p1,p2)) by A4, XCMPLX_1:5;
then A5: |.(p2 - p3).| * (cos (angle p1,p2,p3)) = |.(p2 - p3).| * (cos (angle p3,p1,p2)) by Lm2;
p1 <> p3 by A3, ZFMISC_1:def 5;
then A6: |.(p3 - p1).| <> 0 by Lm1;
|.(p3 - p1).| * (sin (angle p3,p1,p2)) = |.(p3 - p2).| * (sin (angle p1,p2,p3)) by A2, Th6
.= |.(p3 - p1).| * (sin (angle p1,p2,p3)) by A1, Lm2 ;
then A7: sin (angle p3,p1,p2) = sin (angle p1,p2,p3) by A6, XCMPLX_1:5;
p2 <> p3 by A3, ZFMISC_1:def 5;
then |.(p2 - p3).| <> 0 by Lm1;
then cos (angle p1,p2,p3) = cos (angle p3,p1,p2) by A5, XCMPLX_1:5;
hence angle p3,p1,p2 = angle p1,p2,p3 by A7, Th1; :: thesis: verum

end;

suppose A8: not p1,p2,p3 are_mutually_different ; :: thesis: angle p3,p1,p2 = angle p1,p2,p3

per cases ( p1 = p2 or p1 = p3 or p2 = p3 ) by A8, ZFMISC_1:def 5;

suppose p1 = p2 ; :: thesis: angle p3,p1,p2 = angle p1,p2,p3

hence angle p3,p1,p2 = angle p1,p2,p3 by A2; :: thesis: verum

end;

suppose A9: p1 = p3 ; :: thesis: angle p3,p1,p2 = angle p1,p2,p3

then |.(p2 - p3).| = 0 by A1, Lm1;
then p2 = p3 by Lm1;
hence angle p3,p1,p2 = angle p1,p2,p3 by A9; :: thesis: verum

end;

suppose A10: p2 = p3 ; :: thesis: angle p3,p1,p2 = angle p1,p2,p3

then |.(p3 - p1).| = 0 by A1, Lm1;
then p3 = p1 by Lm1;
hence angle p3,p1,p2 = angle p1,p2,p3 by A10; :: thesis: verum

end;

end;

end;

end;