theorem Th30: :: EUCLID_6:30

for p1, p3, p4, p being Point of (TOP-REAL 2)
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) & p3 <> p4 holds
p = p1