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 that
A1: p1 in circle a,b,r and
A2: p2 in circle a,b,r and
A3: p3 in circle a,b,r and
A4: 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).|) )
A5: |.(p3 - p1).| = |.(p1 - p3).| by Lm2;
assume that
A6: p in LSeg p1,p3 and
A7: p in LSeg p2,p4 ; :: thesis: |.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)

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

suppose A8: 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 A8, ZFMISC_1:def 6;

suppose A9: 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 A9; :: thesis: verum

end;

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

then A10: p in {p1} by A6, 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 A7, XBOOLE_0:def 4;
then p in {p2,p4} by A2, A4, TOPREAL9:61;
then A11: ( p = p2 or p = p4 ) by TARSKI:def 2;

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

suppose A12: 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 A12; :: thesis: verum

end;

suppose A13: 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 A5, A13, Lm2; :: thesis: verum

end;

end;

end;

suppose A14: 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 A5, A14, Lm2; :: 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;

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

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

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

suppose A18: 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 A18; :: thesis: verum

end;

suppose A19: 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 A19; :: thesis: verum

end;

end;

end;

suppose A20: 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 A20; :: thesis: verum

end;

end;

end;

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

then A22: p3 <> p4 by ZFMISC_1:def 6;
then A23: euc2cpx p3 <> euc2cpx p4 by EUCLID_3:6;
A24: p2 <> p4 by A21, ZFMISC_1:def 6;
then A25: angle p3,p4,p2 <> PI by A2, A3, A4, A22, Th35;
A26: p1 <> p2 by A21, ZFMISC_1:def 6;
then A27: angle p1,p2,p4 <> PI by A1, A2, A4, A24, Th35;
A28: p1 <> p4 by A21, ZFMISC_1:def 6;
then A29: angle p4,p1,p2 <> PI by A1, A2, A4, A26, Th35;
A30: angle p2,p4,p1 <> PI by A1, A2, A4, A28, A24, Th35;
p2,p4,p1 are_mutually_different by A26, A28, A24, ZFMISC_1:def 5;
then A31: p2,p4,p1 is_a_triangle by A30, A29, A27, Th20;
A32: p2 <> p3 by A21, ZFMISC_1:def 6;
then A33: euc2cpx p2 <> euc2cpx p3 by EUCLID_3:6;
A34: angle p2,p3,p4 <> PI by A2, A3, A4, A32, A22, Th35;
A35: not p2 in LSeg p1,p3

proof

assume A36: p2 in LSeg p1,p3 ; :: thesis: contradiction
not p2 in {p1,p3} by A26, A32, TARSKI:def 2;
then A37: p2 in (LSeg p1,p3) \ {p1,p3} by A36, XBOOLE_0:def 5;
(LSeg p1,p3) \ {p1,p3} c= inside_of_circle a,b,r by A1, A3, TOPREAL9:60;
then ( inside_of_circle a,b,r misses circle a,b,r & p2 in (inside_of_circle a,b,r) /\ (circle a,b,r) ) by A2, A37, TOPREAL9:54, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7; :: thesis: verum

end;

then consider p5 being Point of (TOP-REAL 2) such that
A38: p5 in LSeg p1,p3 and
A39: angle p1,p2,p5 = angle p,p2,p3 by A6, Th28;
A40: angle p4,p2,p3 <> PI by A2, A3, A4, A32, A24, Th35;
then A41: angle p1,p2,p5 <> PI by A6, A7, A35, A39, Th9;
A42: euc2cpx p2 <> euc2cpx p4 by A24, EUCLID_3:6;
A43: p5 <> p1

proof

assume p5 = p1 ; :: thesis: contradiction
then angle p4,p2,p3 = angle p1,p2,p1 by A6, A7, A35, A39, Th9
.= 0 by COMPLEX2:93 ;
hence contradiction by A34, A25, A33, A42, A23, COMPLEX2:101; :: thesis: verum

end;

A44: p5 <> p3

proof

( (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 A45: ( (angle p4,p2,p3) + (angle p3,p2,p4) = 0 or (angle p4,p2,p3) + (angle p3,p2,p4) = 0 + (2 * PI ) ) by COMPLEX2:93;
assume p5 = p3 ; :: thesis: contradiction
then A46: angle p4,p2,p3 = angle p1,p2,p3 by A6, A7, A35, A39, Th9;

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 A45, 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, A2, A4, A26, A28, A24, A46, 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 A46, 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 A46;
hence contradiction by COMPLEX2:84; :: thesis: verum

end;

end;

end;

A47: angle p,p2,p3 = angle p4,p2,p3 by A6, A7, A35, Th9;
A48: 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 A47, A39, 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 A49: ( (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 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 A49, COMPLEX2:84; :: thesis: verum

end;

suppose A50: ( 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 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 A50, COMPLEX2:84; :: thesis: verum

end;

end;

end;

A51: p5 <> p2

proof

A52: (LSeg p1,p3) \ {p1,p3} c= inside_of_circle a,b,r by A1, A3, TOPREAL9:60;
assume A53: p5 = p2 ; :: thesis: contradiction
not p2 in {p1,p3} by A26, A32, TARSKI:def 2;
then p2 in (LSeg p1,p3) \ {p1,p3} by A38, A53, XBOOLE_0:def 5;
then ( inside_of_circle a,b,r misses circle a,b,r & p2 in (inside_of_circle a,b,r) /\ (circle a,b,r) ) by A2, A52, TOPREAL9:54, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7; :: thesis: verum

end;

then A54: p1,p2,p5 are_mutually_different by A26, A43, ZFMISC_1:def 5;
p1 <> p3 by A21, ZFMISC_1:def 6;
then p2,p3,p4,p1 are_mutually_different by A26, A28, A32, A24, A22, ZFMISC_1:def 6;
then A55: angle p2,p1,p3 = angle p2,p4,p3 by A1, A2, A3, A4, A6, A7, Th36;
A56: angle p3,p1,p2 = angle p3,p4,p2

proof

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

suppose A57: 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 A55, A57, EUCLID_3:45; :: thesis: verum

end;

suppose A58: 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 A55, A58, EUCLID_3:46; :: thesis: verum

end;

end;

end;

then A59: angle p5,p1,p2 = angle p3,p4,p2 by A38, A43, Th9;
A60: angle p2,p3,p4 = angle p2,p5,p1

proof

A61: ( euc2cpx p2 <> euc2cpx p5 & euc2cpx p2 <> euc2cpx p1 ) by A26, A51, EUCLID_3:6;
A62: euc2cpx p5 <> euc2cpx p1 by A43, 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 A33, A42, A23, A61, A62, 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 A47, A39, A59; :: thesis: verum

end;

suppose A63: ( ((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

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

end;

suppose A65: ( ((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

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

end;

end;

end;

A67: angle p1,p4,p2 = angle p1,p3,p2 by A1, A2, A3, A4, A6, A7, A21, Th36;
angle p2,p4,p1 = angle p2,p3,p1

proof

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

suppose A68: 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 A67, A68, EUCLID_3:45; :: thesis: verum

end;

suppose A69: 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 A67, A69, EUCLID_3:46; :: thesis: verum

end;

end;

end;

then A70: angle p2,p4,p1 = angle p2,p3,p5 by A38, A44, Th10;
A71: angle p4,p1,p2 = angle p3,p5,p2

proof

A72: ( euc2cpx p2 <> euc2cpx p5 & euc2cpx p3 <> euc2cpx p5 ) by A44, A51, EUCLID_3:6;
A73: ( euc2cpx p4 <> euc2cpx p1 & euc2cpx p2 <> euc2cpx p3 ) by A28, A32, EUCLID_3:6;
A74: ( euc2cpx p2 <> euc2cpx p4 & euc2cpx p2 <> euc2cpx p1 ) by A26, A24, 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 A74, A73, A72, 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 A70, A48; :: thesis: verum

end;

suppose A75: ( ((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

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

end;

suppose A77: ( ((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

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

end;

end;

end;

p2,p3,p5 are_mutually_different by A32, A44, A51, ZFMISC_1:def 5;
then p2,p3,p5 is_a_triangle by A70, A48, A71, A30, A29, A27, Th20;
then |.(p5 - p3).| * |.(p4 - p2).| = |.(p3 - p2).| * |.(p1 - p4).| by A70, A48, A31, Th21;
then |.(p5 - p3).| * |.(p4 - p2).| = |.(p3 - p2).| * |.(p4 - p1).| by Lm2;
then A79: |.(p3 - p5).| * |.(p4 - p2).| = |.(p3 - p2).| * |.(p4 - p1).| by Lm2;
p4,p2,p3 are_mutually_different by A32, A24, A22, ZFMISC_1:def 5;
then A80: p4,p2,p3 is_a_triangle by A40, A34, A25, Th20;
A81: |.(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 A38, A43, A44, Th8
.= sqrt ((|.(p1 - p5).| + |.(p3 - p5).|) ^2 ) by SIN_COS:82
.= |.(p1 - p5).| + |.(p3 - p5).| by SQUARE_1:89 ;
angle p5,p1,p2 <> PI by A2, A3, A4, A24, A22, A38, A43, A56, Th9, Th35;
then p1,p2,p5 is_a_triangle by A34, A60, A41, A54, Th20;
then |.(p1 - p5).| * |.(p2 - p4).| = |.(p2 - p1).| * |.(p4 - p3).| by A47, A39, A59, A80, Th21;
then |.(p1 - p5).| * |.(p4 - p2).| = |.(p2 - p1).| * |.(p4 - p3).| by Lm2;
hence (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|) = (|.(p5 - p1).| * |.(p4 - p2).|) + (|.(p3 - p5).| * |.(p4 - p2).|) by A79, Lm2
.= (|.(p5 - p1).| + |.(p3 - p5).|) * |.(p4 - p2).|
.= |.(p3 - p1).| * |.(p4 - p2).| by A81, Lm2 ;
:: thesis: verum

end;

end;