theorem Th36:
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) &
p1,
p2,
p3,
p4 are_mutually_distinct holds
angle (
p1,
p4,
p2)
= angle (
p1,
p3,
p2)