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
|.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).|
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 |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| )
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 |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| )
assume A2: ( p in LSeg p1,p3 & p in LSeg p2,p4 ) ; :: thesis: |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).|
A3: |.(p1 - p).| = |.(p - p1).| by Lm2;
A4: |.(p2 - p).| = |.(p - p2).| by Lm2;
A5: |.(p3 - p).| = |.(p - p3).| by Lm2;
A6: |.(p4 - p).| = |.(p - p4).| by Lm2;

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

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

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

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

hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A1, A2, Lm22; :: thesis: verum

end;

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

hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A1, A2, Lm23; :: thesis: verum

end;

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

hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A1, A2, A4, A6, Lm22; :: thesis: verum

end;

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

hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A1, A2, A3, A5, Lm22; :: thesis: verum

end;

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

hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A1, A2, Lm23; :: thesis: verum

end;

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

hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A1, A2, A3, A4, A6, Lm22; :: thesis: verum

end;

end;

end;

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

then A9: ( p1 <> p2 & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 & p3 <> p4 ) by ZFMISC_1:def 6;
A10: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;
A11: (LSeg p2,p4) \ {p2,p4} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
A12: (LSeg p1,p3) \ {p1,p3} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
A13: ( p <> p1 & p <> p4 )

proof

assume A14: ( p = p1 or p = p4 ) ; :: thesis: contradiction

per cases ( p = p1 or p = p4 ) by A14;

suppose A15: p = p1 ; :: thesis: contradiction

not p1 in {p2,p4} by A9, TARSKI:def 2;
then p1 in (LSeg p2,p4) \ {p2,p4} by A2, A15, XBOOLE_0:def 5;
then p1 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A11, XBOOLE_0:def 4;
hence contradiction by A10, XBOOLE_0:def 7; :: thesis: verum

end;

suppose A16: p = p4 ; :: thesis: contradiction

not p4 in {p1,p3} by A9, TARSKI:def 2;
then p4 in (LSeg p1,p3) \ {p1,p3} by A2, A16, XBOOLE_0:def 5;
then p4 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A12, XBOOLE_0:def 4;
hence contradiction by A10, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

A17: ( p <> p2 & p <> p3 )

proof

assume A18: ( p = p2 or p = p3 ) ; :: thesis: contradiction

per cases ( p = p3 or p = p2 ) by A18;

suppose A19: p = p3 ; :: thesis: contradiction

not p3 in {p2,p4} by A9, TARSKI:def 2;
then p3 in (LSeg p2,p4) \ {p2,p4} by A2, A19, XBOOLE_0:def 5;
then p3 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A11, XBOOLE_0:def 4;
hence contradiction by A10, XBOOLE_0:def 7; :: thesis: verum

end;

suppose A20: p = p2 ; :: thesis: contradiction

not p2 in {p1,p3} by A9, TARSKI:def 2;
then p2 in (LSeg p1,p3) \ {p1,p3} by A2, A20, XBOOLE_0:def 5;
then p2 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A12, XBOOLE_0:def 4;
hence contradiction by A10, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

A21: angle p1,p4,p = angle p1,p4,p2 by A2, A13, Th10;
A22: angle p,p3,p2 = angle p1,p3,p2 by A2, A17, Th9;
A23: angle p4,p,p1 = angle p2,p,p3 by A2, A13, A17, Th15;
A24: angle p1,p4,p2 = angle p1,p3,p2 by A1, A2, A8, Th36;
A25: p4,p,p1 are_mutually_different by A9, A13, ZFMISC_1:def 5;
A26: angle p4,p,p1 <> PI

proof

assume angle p4,p,p1 = PI ; :: thesis: contradiction
then p in LSeg p1,p4 by Th11;
hence contradiction by A1, A2, A9, A13, Th30; :: thesis: verum

end;

A27: angle p,p1,p4 <> PI

proof

assume angle p,p1,p4 = PI ; :: thesis: contradiction
then angle p3,p1,p4 = PI by A2, A13, Th9;
hence contradiction by A1, A9, Th35; :: thesis: verum

end;

angle p1,p4,p <> PI

proof

assume angle p1,p4,p = PI ; :: thesis: contradiction
then angle p1,p4,p2 = PI by A2, A13, Th10;
hence contradiction by A1, A9, Th35; :: thesis: verum

end;

then A28: p4,p,p1 is_a_triangle by A25, A26, A27, Th20;
A29: p2,p,p3 are_mutually_different by A9, A17, ZFMISC_1:def 5;
A30: angle p2,p,p3 <> PI by A2, A13, A17, A26, Th15;
A31: angle p,p3,p2 <> PI

proof

assume angle p,p3,p2 = PI ; :: thesis: contradiction
then angle p1,p3,p2 = PI by A2, A17, Th9;
hence contradiction by A1, A9, Th35; :: thesis: verum

end;

angle p3,p2,p <> PI

proof

assume angle p3,p2,p = PI ; :: thesis: contradiction
then angle p3,p2,p4 = PI by A2, A17, Th10;
hence contradiction by A1, A9, Th35; :: thesis: verum

end;

then p2,p,p3 is_a_triangle by A29, A30, A31, Th20;
hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A3, A4, A5, A6, A21, A22, A23, A24, A28, Th22; :: thesis: verum

end;

end;