let p1, p2, 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 & p4 in circle a,b,r & p in LSeg p1,p1 & p in LSeg p2,p4 holds
|.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).|
let a, b, r be real number ; :: thesis: ( p1 in circle a,b,r & p2 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p1 & p in LSeg p2,p4 implies |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| )
assume A1: ( p1 in circle a,b,r & p2 in circle a,b,r & p4 in circle a,b,r ) ; :: thesis: ( not p in LSeg p1,p1 or not p in LSeg p2,p4 or |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| )
assume p in LSeg p1,p1 ; :: thesis: ( not p in LSeg p2,p4 or |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| )
then A2: p in {p1} by TOPREAL1:7;
then A3: |.(p1 - p).| = |.(p - p).| by TARSKI:def 1
.= |.(0.REAL 2).| by EUCLID:46
.= 0 by EUCLID:10 ;
assume p in LSeg p2,p4 ; :: thesis: |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).|
then A4: p1 in LSeg p2,p4 by A2, TARSKI:def 1;
A5: (LSeg p2,p4) \ {p2,p4} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
A6: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;

per cases ( ( p1 <> p2 & p1 <> p4 ) or not p1 <> p2 or not p1 <> p4 ) ;

suppose ( p1 <> p2 & p1 <> p4 ) ; :: thesis: |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).|

then not p1 in {p2,p4} by TARSKI:def 2;
then p1 in (LSeg p2,p4) \ {p2,p4} by A4, XBOOLE_0:def 5;
then p1 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A5, XBOOLE_0:def 4;
hence |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| by A6, XBOOLE_0:def 7; :: thesis: verum

end;

suppose A7: ( not p1 <> p2 or not p1 <> p4 ) ; :: thesis: |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).|

per cases ( p1 = p2 or p1 = p4 ) by A7;

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

then |.(p2 - p).| = |.(p1 - p1).| by A2, TARSKI:def 1
.= |.(0.REAL 2).| by EUCLID:46
.= 0 by EUCLID:10 ;
hence |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| by A3; :: thesis: verum

end;

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

then |.(p - p4).| = |.(p1 - p1).| by A2, TARSKI:def 1
.= |.(0.REAL 2).| by EUCLID:46
.= 0 by EUCLID:10 ;
hence |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| by A3; :: thesis: verum

end;

end;

end;

end;