let p1, p3, p4, p be Point of (TOP-REAL 2); :: thesis: for a, b, r being real number 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 number ; :: 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 EUCLID:46
.= 0 by EUCLID_2:61 ;
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;