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
|.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).|
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 |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| )
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 |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| )
A5: |.(p1 - p).| = |.(p - p1).| by Lm2;
A6: |.(p3 - p).| = |.(p - p3).| by Lm2;
A7: ( |.(p2 - p).| = |.(p - p2).| & |.(p4 - p).| = |.(p - p4).| ) by Lm2;
assume that
A8: p in LSeg (p1,p3) and
A9: p in LSeg (p2,p4) ; :: thesis: |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).|

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

suppose A10: not p1,p2,p3,p4 are_mutually_distinct ; :: 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 A10, 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, A3, A4, A8, A9, 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, A4, A8, A9, 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, A3, A8, A9, A7, 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, A4, A8, A9, A5, A6, 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, A3, A8, A9, 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, A8, A9, A5, A7, Lm22; :: thesis: verum

end;

end;

end;

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

then A12: p3 <> p4 by ZFMISC_1:def 6;
A13: p1 <> p2 by A11, ZFMISC_1:def 6;
A14: p2 <> p3 by A11, ZFMISC_1:def 6;
A15: (LSeg (p1,p3)) \ {p1,p3} c= inside_of_circle (a,b,r) by A1, A3, TOPREAL9:60;
A16: inside_of_circle (a,b,r) misses circle (a,b,r) by TOPREAL9:54;
A17: (LSeg (p2,p4)) \ {p2,p4} c= inside_of_circle (a,b,r) by A2, A4, TOPREAL9:60;
A18: ( p <> p2 & p <> p3 )

proof

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

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

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

not p3 in {p2,p4} by A14, A12, TARSKI:def 2;
then p3 in (LSeg (p2,p4)) \ {p2,p4} by A9, A20, XBOOLE_0:def 5;
then p3 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r)) by A3, A17, XBOOLE_0:def 4;
hence contradiction by A16, XBOOLE_0:def 7; :: thesis: verum

end;

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

not p2 in {p1,p3} by A13, A14, TARSKI:def 2;
then p2 in (LSeg (p1,p3)) \ {p1,p3} by A8, A21, XBOOLE_0:def 5;
then p2 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r)) by A2, A15, XBOOLE_0:def 4;
hence contradiction by A16, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

then A22: p2,p,p3 are_mutually_distinct by A14, ZFMISC_1:def 5;
A23: p1 <> p4 by A11, ZFMISC_1:def 6;
A24: ( p <> p1 & p <> p4 )

proof

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

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

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

not p1 in {p2,p4} by A13, A23, TARSKI:def 2;
then p1 in (LSeg (p2,p4)) \ {p2,p4} by A9, A26, XBOOLE_0:def 5;
then p1 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r)) by A1, A17, XBOOLE_0:def 4;
hence contradiction by A16, XBOOLE_0:def 7; :: thesis: verum

end;

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

not p4 in {p1,p3} by A23, A12, TARSKI:def 2;
then p4 in (LSeg (p1,p3)) \ {p1,p3} by A8, A27, XBOOLE_0:def 5;
then p4 in (inside_of_circle (a,b,r)) /\ (circle (a,b,r)) by A4, A15, XBOOLE_0:def 4;
hence contradiction by A16, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

then A28: angle (p4,p,p1) = angle (p2,p,p3) by A8, A9, A18, Th15;
A29: p2 <> p4 by A11, ZFMISC_1:def 6;
A30: angle (p3,p2,p) <> PI

proof

assume angle (p3,p2,p) = PI ; :: thesis: contradiction
then angle (p3,p2,p4) = PI by A9, A18, Th10;
hence contradiction by A2, A3, A4, A14, A29, Th35; :: thesis: verum

end;

A31: p1 <> p3 by A11, ZFMISC_1:def 6;
A32: angle (p,p3,p2) <> PI

proof

assume angle (p,p3,p2) = PI ; :: thesis: contradiction
then angle (p1,p3,p2) = PI by A8, A18, Th9;
hence contradiction by A1, A2, A3, A31, A14, Th35; :: thesis: verum

end;

A33: angle (p,p1,p4) <> PI

proof

assume angle (p,p1,p4) = PI ; :: thesis: contradiction
then angle (p3,p1,p4) = PI by A8, A24, Th9;
hence contradiction by A1, A3, A4, A31, A23, Th35; :: thesis: verum

end;

A34: angle (p,p3,p2) = angle (p1,p3,p2) by A8, A18, Th9;
A35: angle (p1,p4,p) = angle (p1,p4,p2) by A9, A24, Th10;
A36: 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, A4, A9, A13, A24, Th30; :: thesis: verum

end;

then angle (p2,p,p3) <> PI by A8, A9, A24, A18, Th15;
then A37: p2,p,p3 is_a_triangle by A22, A32, A30, Th20;
A38: angle (p1,p4,p) <> PI

proof

assume angle (p1,p4,p) = PI ; :: thesis: contradiction
then angle (p1,p4,p2) = PI by A9, A24, Th10;
hence contradiction by A1, A2, A4, A23, A29, Th35; :: thesis: verum

end;

p4,p,p1 are_mutually_distinct by A23, A24, ZFMISC_1:def 5;
then A39: p4,p,p1 is_a_triangle by A36, A33, A38, Th20;
angle (p1,p4,p2) = angle (p1,p3,p2) by A1, A2, A3, A4, A8, A9, A11, Th36;
hence |.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).| by A5, A6, A7, A35, A34, A28, A39, A37, Th22; :: thesis: verum

end;

end;