let p1, p2, p3, p4 be 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) & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 & not angle (p1,p3,p2) = angle (p1,p4,p2) & not angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI holds
angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI
let a, b, r be Real; ( p1 in circle (a,b,r) & p2 in circle (a,b,r) & p3 in circle (a,b,r) & p4 in circle (a,b,r) & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 & not angle (p1,p3,p2) = angle (p1,p4,p2) & not angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI implies angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )
assume A1:
p1 in circle (a,b,r)
; ( not p2 in circle (a,b,r) or not p3 in circle (a,b,r) or not p4 in circle (a,b,r) or not p1 <> p3 or not p1 <> p4 or not p2 <> p3 or not p2 <> p4 or angle (p1,p3,p2) = angle (p1,p4,p2) or angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI or angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )
set pc = |[a,b]|;
assume A2:
p2 in circle (a,b,r)
; ( not p3 in circle (a,b,r) or not p4 in circle (a,b,r) or not p1 <> p3 or not p1 <> p4 or not p2 <> p3 or not p2 <> p4 or angle (p1,p3,p2) = angle (p1,p4,p2) or angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI or angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )
assume A3:
p3 in circle (a,b,r)
; ( not p4 in circle (a,b,r) or not p1 <> p3 or not p1 <> p4 or not p2 <> p3 or not p2 <> p4 or angle (p1,p3,p2) = angle (p1,p4,p2) or angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI or angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )
assume A4:
p4 in circle (a,b,r)
; ( not p1 <> p3 or not p1 <> p4 or not p2 <> p3 or not p2 <> p4 or angle (p1,p3,p2) = angle (p1,p4,p2) or angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI or angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )
assume that
A5:
p1 <> p3
and
A6:
p1 <> p4
and
A7:
p2 <> p3
and
A8:
p2 <> p4
; ( angle (p1,p3,p2) = angle (p1,p4,p2) or angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI or angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )
per cases
( 2 * (angle (p1,p3,p2)) = angle (p1,|[a,b]|,p2) or 2 * ((angle (p1,p3,p2)) - PI) = angle (p1,|[a,b]|,p2) )
by A1, A2, A3, A5, A7, Th33;
suppose
2
* (angle (p1,p3,p2)) = angle (
p1,
|[a,b]|,
p2)
;
( angle (p1,p3,p2) = angle (p1,p4,p2) or angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI or angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )then
( 2
* (angle (p1,p4,p2)) = 2
* (angle (p1,p3,p2)) or 2
* ((angle (p1,p4,p2)) - PI) = 2
* (angle (p1,p3,p2)) )
by A1, A2, A4, A6, A8, Th33;
hence
(
angle (
p1,
p3,
p2)
= angle (
p1,
p4,
p2) or
angle (
p1,
p3,
p2)
= (angle (p1,p4,p2)) - PI or
angle (
p1,
p3,
p2)
= (angle (p1,p4,p2)) + PI )
;
verum end; suppose
2
* ((angle (p1,p3,p2)) - PI) = angle (
p1,
|[a,b]|,
p2)
;
( angle (p1,p3,p2) = angle (p1,p4,p2) or angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI or angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI )then
( 2
* (angle (p1,p4,p2)) = 2
* ((angle (p1,p3,p2)) - PI) or 2
* ((angle (p1,p4,p2)) - PI) = 2
* ((angle (p1,p3,p2)) - PI) )
by A1, A2, A4, A6, A8, Th33;
hence
(
angle (
p1,
p3,
p2)
= angle (
p1,
p4,
p2) or
angle (
p1,
p3,
p2)
= (angle (p1,p4,p2)) - PI or
angle (
p1,
p3,
p2)
= (angle (p1,p4,p2)) + PI )
;
verum end;