---

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

.....aux..... 
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 leftof zy
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. f1 : Point
17. f2 : Point
18. acb ≅a f1zy
19. acb ≅a f2zy
20. x leftof yz ⇒ f1 leftof yz
21. x leftof yz ⇐ f1 leftof yz
22. x leftof zy ⇐ f1 leftof zy
23. x leftof yz ⇒ f2 leftof yz
24. x leftof yz ⇐ f2 leftof yz
25. x leftof zy ⇐ f2 leftof zy
26. f2 # z
27. z # y
28. f1 # z
29. z # y
30. a' : Point
31. x' : Point
32. z' : Point
33. B(zf2a')
34. B(zyc')
35. B(zf1x')
36. B(zyc')
37. za' ≅ zx'
38. zc' ≅ zc'
39. a'c' ≅ x'c'
40. z' ≡ c'
41. ya' ≅ yx'
42. f2 leftof zy
43. f1 leftof zy
44. f leftof zy
⊢ x' ≡ a'
BY
{ (((Assert x' leftof zy BY
           (InstLemma `left-convex2` [⌜e⌝;⌜z⌝;⌜y⌝;⌜f1⌝;⌜x'⌝]⋅ THEN Auto))
    THEN (Assert a' leftof zy BY
                (InstLemma `left-convex2` [⌜e⌝;⌜z⌝;⌜y⌝;⌜f2⌝;⌜a'⌝]⋅ THEN Auto))
    )
   THEN InstLemma `Euclid-Prop7` [⌜e⌝;⌜z⌝;⌜y⌝;⌜a'⌝;⌜x'⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
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  leftof  zy
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  \mLeftarrow{}{}  f  leftof  zy
16.  f1  :  Point
17.  f2  :  Point
18.  acb  \mcong{}\msuba{}  f1zy
19.  acb  \mcong{}\msuba{}  f2zy
20.  x  leftof  yz  {}\mRightarrow{}  f1  leftof  yz
21.  x  leftof  yz  \mLeftarrow{}{}  f1  leftof  yz
22.  x  leftof  zy  \mLeftarrow{}{}  f1  leftof  zy
23.  x  leftof  yz  {}\mRightarrow{}  f2  leftof  yz
24.  x  leftof  yz  \mLeftarrow{}{}  f2  leftof  yz
25.  x  leftof  zy  \mLeftarrow{}{}  f2  leftof  zy
26.  f2  \#  z
27.  z  \#  y
28.  f1  \#  z
29.  z  \#  y
30.  a'  :  Point
31.  x'  :  Point
32.  z'  :  Point
33.  B(zf2a')
34.  B(zyc')
35.  B(zf1x')
36.  B(zyc')
37.  za'  \mcong{}  zx'
38.  zc'  \mcong{}  zc'
39.  a'c'  \mcong{}  x'c'
40.  z'  \mequiv{}  c'
41.  ya'  \mcong{}  yx'
42.  f2  leftof  zy
43.  f1  leftof  zy
44.  f  leftof  zy
\mvdash{}  x'  \mequiv{}  a'


By

---

Latex:
(((Assert  x'  leftof  zy  BY
                  (InstLemma  `left-convex2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}  THEN  Auto))
    THEN  (Assert  a'  leftof  zy  BY
                            (InstLemma  `left-convex2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}f2\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THEN  Auto))
    )
  THEN  InstLemma  `Euclid-Prop7`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index