let p1, p2, p3, p4, p be Point of (TOP-REAL 2); :: thesis: for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p2,p4 holds
|.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)
let a, b, r be real number ; :: thesis: ( p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p2,p4 implies |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) )
assume A1: ( p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r ) ; :: thesis: ( not p in LSeg p1,p3 or not p in LSeg p2,p4 or |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) )
assume A2: ( p in LSeg p1,p3 & p in LSeg p2,p4 ) ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)
A3: |.(p3 - p1).| = |.(p1 - p3).| by Lm2;

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

suppose A4: not p1,p2,p3,p4 are_mutually_different ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

per cases ( p1 = p2 or p1 = p3 or p1 = p4 or p2 = p3 or p2 = p4 or p3 = p4 ) by A4, ZFMISC_1:def 6;

suppose A5: p1 = p2 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p2 - p1).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A5; :: thesis: verum

end;

suppose p1 = p3 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then A6: p in {p1} by A2, RLTOPSP1:71;
then p in circle a,b,r by A1, TARSKI:def 1;
then p in (LSeg p2,p4) /\ (circle a,b,r) by A2, XBOOLE_0:def 4;
then p in {p2,p4} by A1, TOPREAL9:61;
then A7: ( p = p2 or p = p4 ) by TARSKI:def 2;

per cases ( p1 = p2 or p1 = p4 ) by A6, A7, TARSKI:def 1;

suppose A8: p1 = p2 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p2 - p1).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A8; :: thesis: verum

end;

suppose A9: p1 = p4 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p4 - p1).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A3, A9, Lm2; :: thesis: verum

end;

end;

end;

suppose A10: p1 = p4 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p4 - p1).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A3, A10, Lm2; :: thesis: verum

end;

suppose A11: p2 = p3 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p3 - p2).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A11; :: thesis: verum

end;

suppose p2 = p4 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then A12: p in {p2} by A2, RLTOPSP1:71;
then p in circle a,b,r by A1, TARSKI:def 1;
then p in (LSeg p1,p3) /\ (circle a,b,r) by A2, XBOOLE_0:def 4;
then p in {p1,p3} by A1, TOPREAL9:61;
then A13: ( p = p1 or p = p3 ) by TARSKI:def 2;

per cases ( p1 = p2 or p2 = p3 ) by A12, A13, TARSKI:def 1;

suppose A14: p1 = p2 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p2 - p1).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A14; :: thesis: verum

end;

suppose A15: p2 = p3 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p3 - p2).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A15; :: thesis: verum

end;

end;

end;

suppose A16: p3 = p4 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then |.(p4 - p3).| = 0 by Lm1;
hence |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) by A16; :: thesis: verum

end;

end;

end;

suppose A17: p1,p2,p3,p4 are_mutually_different ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

then A18: ( p1 <> p2 & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 & p3 <> p4 ) by ZFMISC_1:def 6;
A19: not p2 in LSeg p1,p3

proof

assume A20: p2 in LSeg p1,p3 ; :: thesis: contradiction
A21: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;
A22: (LSeg p1,p3) \ {p1,p3} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
not p2 in {p1,p3} by A18, TARSKI:def 2;
then p2 in (LSeg p1,p3) \ {p1,p3} by A20, XBOOLE_0:def 5;
then p2 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A22, XBOOLE_0:def 4;
hence contradiction by A21, XBOOLE_0:def 7; :: thesis: verum

end;

then A23: angle p,p2,p3 = angle p4,p2,p3 by A2, Th9;
consider p5 being Point of (TOP-REAL 2) such that
A24: ( p5 in LSeg p1,p3 & angle p1,p2,p5 = angle p,p2,p3 ) by A2, A19, Th28;
A25: ( angle p4,p2,p3 <> PI & angle p2,p3,p4 <> PI & angle p3,p4,p2 <> PI ) by A1, A18, Th35;
A26: ( euc2cpx p2 <> euc2cpx p3 & euc2cpx p2 <> euc2cpx p4 & euc2cpx p3 <> euc2cpx p4 ) by A18, EUCLID_3:6;
A27: p5 <> p1

proof

assume p5 = p1 ; :: thesis: contradiction
then angle p4,p2,p3 = angle p1,p2,p1 by A2, A19, A24, Th9
.= 0 by COMPLEX2:93 ;
hence contradiction by A25, A26, COMPLEX2:101; :: thesis: verum

end;

A28: p5 <> p3

proof

assume p5 = p3 ; :: thesis: contradiction
then A29: angle p4,p2,p3 = angle p1,p2,p3 by A2, A19, A24, Th9;
( (angle p4,p2,p3) + (angle p3,p2,p4) = angle p4,p2,p4 or (angle p4,p2,p3) + (angle p3,p2,p4) = (angle p4,p2,p4) + (2 * PI ) ) by Th4;
then A30: ( (angle p4,p2,p3) + (angle p3,p2,p4) = 0 or (angle p4,p2,p3) + (angle p3,p2,p4) = 0 + (2 * PI ) ) by COMPLEX2:93;

per cases ( ( (angle p4,p2,p3) + (angle p3,p2,p4) = 0 & (angle p1,p2,p3) + (angle p3,p2,p4) = angle p1,p2,p4 ) or ( (angle p4,p2,p3) + (angle p3,p2,p4) = 2 * PI & (angle p1,p2,p3) + (angle p3,p2,p4) = (angle p1,p2,p4) + (2 * PI ) ) or ( (angle p4,p2,p3) + (angle p3,p2,p4) = 2 * PI & (angle p1,p2,p3) + (angle p3,p2,p4) = angle p1,p2,p4 ) or ( (angle p4,p2,p3) + (angle p3,p2,p4) = 0 & (angle p1,p2,p3) + (angle p3,p2,p4) = (angle p1,p2,p4) + (2 * PI ) ) ) by A30, Th4;

suppose ( ( (angle p4,p2,p3) + (angle p3,p2,p4) = 0 & (angle p1,p2,p3) + (angle p3,p2,p4) = angle p1,p2,p4 ) or ( (angle p4,p2,p3) + (angle p3,p2,p4) = 2 * PI & (angle p1,p2,p3) + (angle p3,p2,p4) = (angle p1,p2,p4) + (2 * PI ) ) ) ; :: thesis: contradiction

hence contradiction by A1, A18, A29, Th37; :: thesis: verum

end;

suppose ( (angle p4,p2,p3) + (angle p3,p2,p4) = 2 * PI & (angle p1,p2,p3) + (angle p3,p2,p4) = angle p1,p2,p4 ) ; :: thesis: contradiction

hence contradiction by A29, COMPLEX2:84; :: thesis: verum

end;

suppose ( (angle p4,p2,p3) + (angle p3,p2,p4) = 0 & (angle p1,p2,p3) + (angle p3,p2,p4) = (angle p1,p2,p4) + (2 * PI ) ) ; :: thesis: contradiction

then angle p1,p2,p4 = - (2 * PI ) by A29;
hence contradiction by COMPLEX2:84; :: thesis: verum

end;

end;

end;

A31: p5 <> p2

proof

assume A32: p5 = p2 ; :: thesis: contradiction
A33: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;
A34: (LSeg p1,p3) \ {p1,p3} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
not p2 in {p1,p3} by A18, TARSKI:def 2;
then p2 in (LSeg p1,p3) \ {p1,p3} by A24, A32, XBOOLE_0:def 5;
then p2 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A34, XBOOLE_0:def 4;
hence contradiction by A33, XBOOLE_0:def 7; :: thesis: verum

end;

p2,p3,p4,p1 are_mutually_different by A18, ZFMISC_1:def 6;
then A35: angle p2,p1,p3 = angle p2,p4,p3 by A1, A2, Th36;
A36: angle p3,p1,p2 = angle p3,p4,p2

proof

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

suppose A37: angle p2,p1,p3 = 0 ; :: thesis: angle p3,p1,p2 = angle p3,p4,p2

then angle p3,p1,p2 = 0 by EUCLID_3:45;
hence angle p3,p1,p2 = angle p3,p4,p2 by A35, A37, EUCLID_3:45; :: thesis: verum

end;

suppose A38: angle p2,p1,p3 <> 0 ; :: thesis: angle p3,p1,p2 = angle p3,p4,p2

then angle p3,p1,p2 = (2 * PI ) - (angle p2,p1,p3) by EUCLID_3:46;
hence angle p3,p1,p2 = angle p3,p4,p2 by A35, A38, EUCLID_3:46; :: thesis: verum

end;

end;

end;

then A39: angle p5,p1,p2 = angle p3,p4,p2 by A24, A27, Th9;
A40: angle p1,p4,p2 = angle p1,p3,p2 by A1, A2, A17, Th36;
angle p2,p4,p1 = angle p2,p3,p1

proof

per cases ( angle p1,p4,p2 = 0 or angle p1,p4,p2 <> 0 ) ;

suppose A41: angle p1,p4,p2 = 0 ; :: thesis: angle p2,p4,p1 = angle p2,p3,p1

then angle p2,p4,p1 = 0 by EUCLID_3:45;
hence angle p2,p4,p1 = angle p2,p3,p1 by A40, A41, EUCLID_3:45; :: thesis: verum

end;

suppose A42: angle p1,p4,p2 <> 0 ; :: thesis: angle p2,p4,p1 = angle p2,p3,p1

then angle p2,p4,p1 = (2 * PI ) - (angle p1,p4,p2) by EUCLID_3:46;
hence angle p2,p4,p1 = angle p2,p3,p1 by A40, A42, EUCLID_3:46; :: thesis: verum

end;

end;

end;

then A43: angle p2,p4,p1 = angle p2,p3,p5 by A24, A28, Th10;
A44: angle p5,p2,p3 = angle p1,p2,p4

proof

per cases ( ( angle p5,p2,p3 = (angle p5,p2,p4) + (angle p4,p2,p3) & angle p1,p2,p4 = (angle p4,p2,p3) + (angle p5,p2,p4) ) or ( (angle p5,p2,p3) + (2 * PI ) = (angle p5,p2,p4) + (angle p4,p2,p3) & (angle p1,p2,p4) + (2 * PI ) = (angle p4,p2,p3) + (angle p5,p2,p4) ) or ( (angle p5,p2,p3) + (2 * PI ) = (angle p5,p2,p4) + (angle p4,p2,p3) & angle p1,p2,p4 = (angle p4,p2,p3) + (angle p5,p2,p4) ) or ( angle p5,p2,p3 = (angle p5,p2,p4) + (angle p4,p2,p3) & (angle p1,p2,p4) + (2 * PI ) = (angle p4,p2,p3) + (angle p5,p2,p4) ) ) by A23, A24, Th4;

suppose ( ( angle p5,p2,p3 = (angle p5,p2,p4) + (angle p4,p2,p3) & angle p1,p2,p4 = (angle p4,p2,p3) + (angle p5,p2,p4) ) or ( (angle p5,p2,p3) + (2 * PI ) = (angle p5,p2,p4) + (angle p4,p2,p3) & (angle p1,p2,p4) + (2 * PI ) = (angle p4,p2,p3) + (angle p5,p2,p4) ) ) ; :: thesis: angle p5,p2,p3 = angle p1,p2,p4

hence angle p5,p2,p3 = angle p1,p2,p4 ; :: thesis: verum

end;

suppose A45: ( (angle p5,p2,p3) + (2 * PI ) = (angle p5,p2,p4) + (angle p4,p2,p3) & angle p1,p2,p4 = (angle p4,p2,p3) + (angle p5,p2,p4) ) ; :: thesis: angle p5,p2,p3 = angle p1,p2,p4

( angle p5,p2,p3 >= 0 & angle p1,p2,p4 < 2 * PI ) by COMPLEX2:84;
then (angle p5,p2,p3) + (2 * PI ) >= 0 + (2 * PI ) by XREAL_1:8;
hence angle p5,p2,p3 = angle p1,p2,p4 by A45, COMPLEX2:84; :: thesis: verum

end;

suppose A46: ( angle p5,p2,p3 = (angle p5,p2,p4) + (angle p4,p2,p3) & (angle p1,p2,p4) + (2 * PI ) = (angle p4,p2,p3) + (angle p5,p2,p4) ) ; :: thesis: angle p5,p2,p3 = angle p1,p2,p4

( angle p5,p2,p3 < 2 * PI & angle p1,p2,p4 >= 0 ) by COMPLEX2:84;
then (angle p1,p2,p4) + (2 * PI ) >= 0 + (2 * PI ) by XREAL_1:8;
hence angle p5,p2,p3 = angle p1,p2,p4 by A46, COMPLEX2:84; :: thesis: verum

end;

end;

end;

angle p2,p3,p4 = angle p2,p5,p1

proof

A47: ( euc2cpx p2 <> euc2cpx p5 & euc2cpx p2 <> euc2cpx p1 & euc2cpx p5 <> euc2cpx p1 ) by A18, A27, A31, EUCLID_3:6;

per cases ( ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = PI ) or ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = 5 * PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = 5 * PI ) or ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = 5 * PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = PI ) or ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = 5 * PI ) ) by A26, A47, COMPLEX2:102;

suppose ( ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = PI ) or ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = 5 * PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = 5 * PI ) ) ; :: thesis: angle p2,p3,p4 = angle p2,p5,p1

hence angle p2,p3,p4 = angle p2,p5,p1 by A23, A24, A39; :: thesis: verum

end;

suppose ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = 5 * PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = PI ) ; :: thesis: angle p2,p3,p4 = angle p2,p5,p1

then A48: (angle p2,p3,p4) - (angle p2,p5,p1) = 4 * PI by A23, A24, A39;
( angle p2,p3,p4 < 2 * PI & angle p2,p5,p1 >= 0 ) by COMPLEX2:84;
then (angle p2,p3,p4) - (angle p2,p5,p1) < (2 * PI ) - 0 by XREAL_1:16;
hence angle p2,p3,p4 = angle p2,p5,p1 by A48, XREAL_1:66; :: thesis: verum

end;

suppose ( ((angle p2,p3,p4) + (angle p3,p4,p2)) + (angle p4,p2,p3) = PI & ((angle p2,p5,p1) + (angle p5,p1,p2)) + (angle p1,p2,p5) = 5 * PI ) ; :: thesis: angle p2,p3,p4 = angle p2,p5,p1

then A49: (angle p2,p5,p1) - (angle p2,p3,p4) = 4 * PI by A23, A24, A39;
( angle p2,p5,p1 < 2 * PI & angle p2,p3,p4 >= 0 ) by COMPLEX2:84;
then (angle p2,p5,p1) - (angle p2,p3,p4) < (2 * PI ) - 0 by XREAL_1:16;
hence angle p2,p3,p4 = angle p2,p5,p1 by A49, XREAL_1:66; :: thesis: verum

end;

end;

end;

then A50: ( angle p1,p2,p5 <> PI & angle p2,p5,p1 <> PI & angle p5,p1,p2 <> PI ) by A2, A19, A24, A25, A27, A36, Th9;
( p1,p2,p5 are_mutually_different & p4,p2,p3 are_mutually_different ) by A18, A27, A31, ZFMISC_1:def 5;
then A51: ( p1,p2,p5 is_a_triangle & p4,p2,p3 is_a_triangle ) by A25, A50, Th20;
A52: angle p4,p1,p2 = angle p3,p5,p2

proof

A53: ( euc2cpx p2 <> euc2cpx p4 & euc2cpx p2 <> euc2cpx p1 & euc2cpx p4 <> euc2cpx p1 ) by A18, EUCLID_3:6;
A54: ( euc2cpx p2 <> euc2cpx p3 & euc2cpx p2 <> euc2cpx p5 & euc2cpx p3 <> euc2cpx p5 ) by A18, A28, A31, EUCLID_3:6;

per cases ( ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = PI ) or ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = 5 * PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = 5 * PI ) or ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = 5 * PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = PI ) or ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = 5 * PI ) ) by A53, A54, COMPLEX2:102;

suppose ( ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = PI ) or ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = 5 * PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = 5 * PI ) ) ; :: thesis: angle p4,p1,p2 = angle p3,p5,p2

hence angle p4,p1,p2 = angle p3,p5,p2 by A43, A44; :: thesis: verum

end;

suppose ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = 5 * PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = PI ) ; :: thesis: angle p4,p1,p2 = angle p3,p5,p2

then A55: (angle p4,p1,p2) - (angle p3,p5,p2) = 4 * PI by A43, A44;
( angle p4,p1,p2 < 2 * PI & angle p3,p5,p2 >= 0 ) by COMPLEX2:84;
then (angle p4,p1,p2) - (angle p3,p5,p2) < (2 * PI ) - 0 by XREAL_1:16;
hence angle p4,p1,p2 = angle p3,p5,p2 by A55, XREAL_1:66; :: thesis: verum

end;

suppose ( ((angle p2,p4,p1) + (angle p4,p1,p2)) + (angle p1,p2,p4) = PI & ((angle p2,p3,p5) + (angle p3,p5,p2)) + (angle p5,p2,p3) = 5 * PI ) ; :: thesis: angle p4,p1,p2 = angle p3,p5,p2

then A56: (angle p3,p5,p2) - (angle p4,p1,p2) = 4 * PI by A43, A44;
( angle p3,p5,p2 < 2 * PI & angle p4,p1,p2 >= 0 ) by COMPLEX2:84;
then (angle p3,p5,p2) - (angle p4,p1,p2) < (2 * PI ) - 0 by XREAL_1:16;
hence angle p4,p1,p2 = angle p3,p5,p2 by A56, XREAL_1:66; :: thesis: verum

end;

end;

end;

A57: ( angle p2,p4,p1 <> PI & angle p4,p1,p2 <> PI & angle p1,p2,p4 <> PI ) by A1, A18, Th35;
( p2,p3,p5 are_mutually_different & p2,p4,p1 are_mutually_different ) by A18, A28, A31, ZFMISC_1:def 5;
then A58: ( p2,p3,p5 is_a_triangle & p2,p4,p1 is_a_triangle ) by A43, A44, A52, A57, Th20;
|.(p1 - p5).| * |.(p2 - p4).| = |.(p2 - p1).| * |.(p4 - p3).| by A23, A24, A39, A51, Th21;
then A59: |.(p1 - p5).| * |.(p4 - p2).| = |.(p2 - p1).| * |.(p4 - p3).| by Lm2;
|.(p5 - p3).| * |.(p4 - p2).| = |.(p3 - p2).| * |.(p1 - p4).| by A43, A44, A58, Th21;
then |.(p5 - p3).| * |.(p4 - p2).| = |.(p3 - p2).| * |.(p4 - p1).| by Lm2;
then A60: |.(p3 - p5).| * |.(p4 - p2).| = |.(p3 - p2).| * |.(p4 - p1).| by Lm2;
A61: |.(p3 - p1).| = sqrt (|.(p3 - p1).| ^2 ) by SQUARE_1:89
.= sqrt (((|.(p1 - p5).| ^2 ) + (|.(p3 - p5).| ^2 )) - (((2 * |.(p1 - p5).|) * |.(p3 - p5).|) * (cos (angle p1,p5,p3)))) by Th7
.= sqrt (((|.(p1 - p5).| ^2 ) + (|.(p3 - p5).| ^2 )) - (((2 * |.(p1 - p5).|) * |.(p3 - p5).|) * (cos PI ))) by A24, A27, A28, Th8
.= sqrt ((|.(p1 - p5).| + |.(p3 - p5).|) ^2 ) by SIN_COS:82
.= |.(p1 - p5).| + |.(p3 - p5).| by SQUARE_1:89 ;
thus (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) = (|.(p5 - p1).| * |.(p4 - p2).|) + (|.(p3 - p5).| * |.(p4 - p2).|) by A59, A60, Lm2
.= (|.(p5 - p1).| + |.(p3 - p5).|) * |.(p4 - p2).|
.= |.(p3 - p1).| * |.(p4 - p2).| by A61, Lm2 ; :: thesis: verum

end;

end;