theorem Th31:
for
p1,
p2,
p,
pc 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) &
p in circle (
a,
b,
r) &
pc = |[a,b]| &
pc in LSeg (
p,
p2) &
p1 <> p & not 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) holds
2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2)