---

Step * 1 of Lemma geo-left-out-better-1

.....assertion..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. b' : Point
5. p : Point
6. p leftof ba
7. b' # a
8. ¬((¬B(ab'b)) ∧ (¬B(abb')))
9. p # ba
10. Colinear(a;b;b')
11. p leftof ab'
⊢ False
BY
{ ((InstLemma `geo-left-out-better` [⌜e⌝;⌜b'⌝;⌜a⌝;⌜b⌝;⌜p⌝]⋅ THEN EAuto 1)
   THEN InstLemma `not-left-and-right` [⌜e⌝;⌜p⌝;⌜a⌝;⌜b⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  b'  :  Point
5.  p  :  Point
6.  p  leftof  ba
7.  b'  \#  a
8.  \mneg{}((\mneg{}B(ab'b))  \mwedge{}  (\mneg{}B(abb')))
9.  p  \#  ba
10.  Colinear(a;b;b')
11.  p  leftof  ab'
\mvdash{}  False


By

---

Latex:
((InstLemma  `geo-left-out-better`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
  THEN  InstLemma  `not-left-and-right`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index