---

Step * 2 1 1 3 of Lemma unique-angles-in-half-plane


1. e : EuclideanPlane
2. c' : Point
3. a : Point
4. b : Point
5. c : Point
6. x : Point
7. y : Point
8. z : Point
9. a # bc
10. x # yz
11. f : Point
12. acb ≅a fzy
13. x leftof yz ⇒ f leftof yz
14. x leftof yz ⇐ f leftof yz
15. x leftof zy ⇒ f leftof zy
16. x leftof zy ⇐ f leftof zy
17. f1 : Point
18. f2 : Point
19. acb ≅a f1zy
20. acb ≅a f2zy
21. x leftof yz ⇒ f1 leftof yz
22. x leftof yz ⇐ f1 leftof yz
23. x leftof zy ⇒ f1 leftof zy
24. x leftof zy ⇐ f1 leftof zy
25. x leftof yz ⇒ f2 leftof yz
26. x leftof yz ⇐ f2 leftof yz
27. x leftof zy ⇒ f2 leftof zy
28. x leftof zy ⇐ f2 leftof zy
29. f2 # z
30. z # y
31. f1 # z
32. z # y
33. a' : Point
34. x' : Point
35. z' : Point
36. B(zf2a')
37. B(zyc')
38. B(zf1x')
39. B(zyc')
40. za' ≅ zx'
41. zc' ≅ zc'
42. a'c' ≅ x'c'
43. z' ≡ c'
44. ya' ≅ yx'
45. x' ≡ a'
⊢ Colinear(z;f1;f2)
BY
{ (D 9 THEN D 10 THEN EliminatePoint (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  c'  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  x  :  Point
7.  y  :  Point
8.  z  :  Point
9.  a  \#  bc
10.  x  \#  yz
11.  f  :  Point
12.  acb  \mcong{}\msuba{}  fzy
13.  x  leftof  yz  {}\mRightarrow{}  f  leftof  yz
14.  x  leftof  yz  \mLeftarrow{}{}  f  leftof  yz
15.  x  leftof  zy  {}\mRightarrow{}  f  leftof  zy
16.  x  leftof  zy  \mLeftarrow{}{}  f  leftof  zy
17.  f1  :  Point
18.  f2  :  Point
19.  acb  \mcong{}\msuba{}  f1zy
20.  acb  \mcong{}\msuba{}  f2zy
21.  x  leftof  yz  {}\mRightarrow{}  f1  leftof  yz
22.  x  leftof  yz  \mLeftarrow{}{}  f1  leftof  yz
23.  x  leftof  zy  {}\mRightarrow{}  f1  leftof  zy
24.  x  leftof  zy  \mLeftarrow{}{}  f1  leftof  zy
25.  x  leftof  yz  {}\mRightarrow{}  f2  leftof  yz
26.  x  leftof  yz  \mLeftarrow{}{}  f2  leftof  yz
27.  x  leftof  zy  {}\mRightarrow{}  f2  leftof  zy
28.  x  leftof  zy  \mLeftarrow{}{}  f2  leftof  zy
29.  f2  \#  z
30.  z  \#  y
31.  f1  \#  z
32.  z  \#  y
33.  a'  :  Point
34.  x'  :  Point
35.  z'  :  Point
36.  B(zf2a')
37.  B(zyc')
38.  B(zf1x')
39.  B(zyc')
40.  za'  \mcong{}  zx'
41.  zc'  \mcong{}  zc'
42.  a'c'  \mcong{}  x'c'
43.  z'  \mequiv{}  c'
44.  ya'  \mcong{}  yx'
45.  x'  \mequiv{}  a'
\mvdash{}  Colinear(z;f1;f2)


By

---

Latex:
(D  9  THEN  D  10  THEN  EliminatePoint  (-1)  THEN  Auto)

---

Home Index