let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for a, b, r being real number 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 number ; :: thesis: ( 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
; :: thesis: ( 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 )
assume A2:
p2 in circle a,b,r
; :: thesis: ( 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
; :: thesis: ( 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
; :: thesis: ( 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 A5:
( p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 )
; :: thesis: ( 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]|;
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, Th33;
suppose
2
* (angle p1,p3,p2) = angle p1,
|[a,b]|,
p2
;
:: thesis: ( 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, A5, 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 )
;
:: thesis: verum end; suppose
2
* ((angle p1,p3,p2) - PI ) = angle p1,
|[a,b]|,
p2
;
:: thesis: ( 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, A5, 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 )
;
:: thesis: verum end;