let p1, p2, 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) & 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; :: 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:70;
then A6: |.(p1 - p).| = |.(p - p).| by TARSKI:def 1
.= |.(0. (TOP-REAL 2)).| by RLVECT_1:5
.= |.(0* 2).| by EUCLID:70
.= 0 by EUCLID:7 ;
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 RLVECT_1:5
.= |.(0* 2).| by EUCLID:70
.= 0 by EUCLID:7 ;
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 RLVECT_1:5
.= |.(0* 2).| by EUCLID:70
.= 0 by EUCLID:7 ;
hence |.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).| by A6; :: thesis: verum

end;

end;

end;

end;