let p1, p3, p4, p be Point of (TOP-REAL 2); :: thesis: for a, b, r being Real st p1 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 (p1,p4) holds
|.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).|
let a, b, r be Real; :: thesis: ( p1 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 (p1,p4) implies |.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).| )
assume A1: ( p1 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 (p1,p4) or |.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).| )
assume A2: ( p in LSeg (p1,p3) & p in LSeg (p1,p4) ) ; :: thesis: |.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).|

per cases ( p3 <> p4 or p3 = p4 ) ;

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

then p = p1 by A1, A2, Th30;
then |.(p1 - p).| = |.(0. (TOP-REAL 2)).| by RLVECT_1:5
.= 0 by EUCLID_2:39 ;
hence |.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).| ; :: thesis: verum

end;

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

hence |.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).| ; :: thesis: verum

end;

end;