1. a k c are collinear (by assumption)
2. a l b are collinear (by assumption)
3. |o a| = |o b| (by assumption)
4. |o p| = |o a| (by assumption)
5. |o b| = |o p| (by calculation 3 4)
|o b| = |o a| (by 3: |o a| = |o b|)
= |o p| (by 4: |o p| = |o a|)
6. ∠o b p = ∠b p o (by isosceles triangle 5)
7. |o a| = |o c| (by assumption)
8. |o p| = |o c| (by calculation 4 7)
|o p| = |o a| (by 4: |o p| = |o a|)
= |o c| (by 7: |o a| = |o c|)
9. ∠o c p = ∠c p o (by isosceles triangle 8)
10. |o b| = |o a| (by calculation 3)
|o b| = |o a| (by 3: |o a| = |o b|)
11. ∠a b o = ∠o a b (by isosceles triangle 10)
12. ∠a c o = ∠o a c (by isosceles triangle 7)
13. b d c are collinear (by assumption)
14. x b c are collinear (by assumption)
15. b x d c are collinear (by merge lines 13 14)
16. y b c are collinear (by assumption)
17. b x d y c are collinear (by merge lines 15 16)
18. ∠y b i = ∠d b i (by calculation 15 17)
d(i b) + -1*d(y b) = d(i b) + -1*d(b d) (∠y b i = ∠d b i)
1 ×    d(y b) + -1*d(b d) = 0        (17: b x d y c are collinear)
19. ∠a b i = ∠i b c (by assumption)
20. i d ⊥ b c (by assumption)
21. y t2 || a b (by assumption)
22. |i t2| = |i d| (by assumption)
23. |i y| / |i d| = |i y| / |i t2| (by calculation 22)
|y i| / |d i| = |y i| / |i t2| (by 22: |i t2| = |i d|)
24. y t2 ⊥ t2 i (by assumption)
25. ∠y t2 i = ∠i d y (by calculation 17 20 24)
d(i t2) + -1*d(t2 y) = d(y d) + -1*d(i d) (∠y t2 i = ∠i d y)
1 ×    d(t2 y) + -1*d(i t2) = 1/2*pi        (24: y t2 ⊥ t2 i)
1 ×    d(y d) + -1*d(c b) = 0        (17: b x d y c are collinear)
-1 ×    d(i d) + -1*d(c b) = 1/2*pi        (20: i d ⊥ b c)
26. |i t2|