let p1, p2, p3, p4, p be Point of (TOP-REAL 2); :: thesis: for a, b, r being Real 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; :: 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_distinct or p1,p2,p3,p4 are_mutually_distinct ) ;

suppose A8: not p1,p2,p3,p4 are_mutually_distinct ; :: 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:70;
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:70;
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_distinct ; :: 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:4;
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_distinct 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:4;
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:4;
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:79 ;
hence contradiction by A34, A25, A33, A42, A23, COMPLEX2:87; :: 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:79;
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:70; :: 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:70; :: 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:70;
then (angle (p5,p2,p3)) + (2 * PI) >= 0 + (2 * PI) by XREAL_1:6;
hence angle (p5,p2,p3) = angle (p1,p2,p4) by A49, COMPLEX2:70; :: 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:70;
then (angle (p1,p2,p4)) + (2 * PI) >= 0 + (2 * PI) by XREAL_1:6;
hence angle (p5,p2,p3) = angle (p1,p2,p4) by A50, COMPLEX2:70; :: 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_distinct by A26, A43, ZFMISC_1:def 5;
p1 <> p3 by A21, ZFMISC_1:def 6;
then p2,p3,p4,p1 are_mutually_distinct 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:36;
hence angle (p3,p1,p2) = angle (p3,p4,p2) by A55, A57, EUCLID_3:36; :: 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:37;
hence angle (p3,p1,p2) = angle (p3,p4,p2) by A55, A58, EUCLID_3:37; :: 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:4;
A62: euc2cpx p5 <> euc2cpx p1 by A43, EUCLID_3:4;

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:88;

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:70;
then A64: (angle (p2,p3,p4)) - (angle (p2,p5,p1)) < (2 * PI) - 0 by XREAL_1:14;
(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:64; :: 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:70;
then A66: (angle (p2,p5,p1)) - (angle (p2,p3,p4)) < (2 * PI) - 0 by XREAL_1:14;
(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:64; :: 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:36;
hence angle (p2,p4,p1) = angle (p2,p3,p1) by A67, A68, EUCLID_3:36; :: 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:37;
hence angle (p2,p4,p1) = angle (p2,p3,p1) by A67, A69, EUCLID_3:37; :: 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:4;
A73: ( euc2cpx p4 <> euc2cpx p1 & euc2cpx p2 <> euc2cpx p3 ) by A28, A32, EUCLID_3:4;
A74: ( euc2cpx p2 <> euc2cpx p4 & euc2cpx p2 <> euc2cpx p1 ) by A26, A24, EUCLID_3:4;

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:88;

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:70;
then A76: (angle (p4,p1,p2)) - (angle (p3,p5,p2)) < (2 * PI) - 0 by XREAL_1:14;
(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:64; :: 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:70;
then A78: (angle (p3,p5,p2)) - (angle (p4,p1,p2)) < (2 * PI) - 0 by XREAL_1:14;
(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:64; :: thesis: verum

end;

end;

end;

p2,p3,p5 are_mutually_distinct 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_distinct 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:22
.= 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:77
.= |.(p1 - p5).| + |.(p3 - p5).| by SQUARE_1:22 ;
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;