let p1, p2, p3 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_distinct or not p1,p2,p3 are_mutually_distinct ) ;
suppose A3: p1,p2,p3 are_mutually_distinct ; :: 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_distinct ; :: 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;