theorem :: EUCLID_6:38

for p1, p2, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being Real st p1 in circle (a,b,r) & p2 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 (p2,p4) holds
|.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).|