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 that
A1: p1 in circle a,b,r and
A2: ( 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).| )
A3: (LSeg p2,p4) \ {p2,p4} c= inside_of_circle a,b,r by A2, TOPREAL9:60;
A4: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;
assume p in LSeg p1,p1 ; :: thesis: ( not p in LSeg p2,p4 or |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| )
then A5: p in {p1} by RLTOPSP1:71;
then A6: |.(p1 - p).| = |.(p - p).| by TARSKI:def 1
.= |.(0. (TOP-REAL 2)).| by EUCLID:46
.= |.(0* 2).| by EUCLID:74
.= 0 by EUCLID:10 ;
assume p in LSeg p2,p4 ; :: thesis: |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).|
then A7: p1 in LSeg p2,p4 by A5, TARSKI:def 1;

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 A7, XBOOLE_0:def 5;
then p1 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A3, XBOOLE_0:def 4;
hence |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| by A4, XBOOLE_0:def 7; :: thesis: verum

end;

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

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

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

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

end;

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

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

end;

end;

end;

end;