---

Step * 1 1 1 1 3 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
22. p leftof ab ⇐ d leftof ab
23. p leftof ba
⊢ d leftof ba
BY
{ ((InstLemma `geo-left-out-1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜b'⌝;⌜p⌝]⋅ THEN EAuto 1)
   THEN (InstLemma `left-convex2` [⌜e⌝;⌜b'⌝;⌜a⌝;⌜p⌝;⌜c'⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-left-out-3` [⌜e⌝;⌜a⌝;⌜b'⌝;⌜c'⌝;⌜c⌝]⋅ THENA EAuto 1)
   THEN (InstLemma `geo-left-out-1` [⌜e⌝;⌜a⌝;⌜b'⌝;⌜b⌝;⌜c⌝]⋅ THEN EAuto 1)
   THEN InstLemma `geo-left-out-2` [⌜e⌝;⌜a⌝;⌜b⌝;⌜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  {}\mRightarrow{}  d  leftof  ab
22.  p  leftof  ab  \mLeftarrow{}{}  d  leftof  ab
23.  p  leftof  ba
\mvdash{}  d  leftof  ba


By

---

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

---

Home Index