---

Step * 1 1 1 1 1 of Lemma interior-angles-unique

.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. a # bc
10. out(b dc)
11. out(a bb')
12. out(a cc')
13. B(b'pc')
14. p # c'
15. bad < bac
16. bap ≅a bad
17. a # p
18. b # p
19. b' # p
20. b # ap
21. p leftof ab
⊢ d leftof ab
BY
{ ((Assert p leftof ab' BY
          (InstLemma `geo-left-out` [⌜e⌝;⌜b⌝;⌜a⌝;⌜b'⌝;⌜p⌝]⋅ THEN EAuto 1))
   THEN (InstLemma `left-convex` [⌜e⌝;⌜a⌝;⌜b'⌝;⌜p⌝;⌜c'⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-left-out-2` [⌜e⌝;⌜b'⌝;⌜a⌝;⌜c'⌝;⌜c⌝]⋅ THENA EAuto 1)
   THEN (InstLemma `geo-left-out` [⌜e⌝;⌜b'⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA EAuto 1)
   THEN InstLemma `geo-left-out-3` [⌜e⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜d⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
.....aux..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  b'  :  Point
7.  c'  :  Point
8.  p  :  Point
9.  a  \#  bc
10.  out(b  dc)
11.  out(a  bb')
12.  out(a  cc')
13.  B(b'pc')
14.  p  \#  c'
15.  bad  <  bac
16.  bap  \mcong{}\msuba{}  bad
17.  a  \#  p
18.  b  \#  p
19.  b'  \#  p
20.  b  \#  ap
21.  p  leftof  ab
\mvdash{}  d  leftof  ab


By

---

Latex:
((Assert  p  leftof  ab'  BY
                (InstLemma  `geo-left-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
  THEN  (InstLemma  `left-convex`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-left-out-2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  (InstLemma  `geo-left-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  InstLemma  `geo-left-out-3`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index