---

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


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a' : Point
5. p : Point
6. p leftof ba
7. b # a'
8. ¬((¬B(baa')) ∧ (¬B(ba'a)))
9. p # ba
10. Colinear(b;a;a')
11. p leftof a'b
⊢ p leftof ba'
BY
{ (D -4 THEN RepeatFor 2 ((D 0 THENA Auto)) THEN InstLemma `left-convex` [⌜e⌝;⌜p⌝;⌜b⌝;⌜a⌝;⌜a'⌝]⋅ THEN EAuto 2) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a' : Point
5. p : Point
6. p leftof ba
7. b # a'
8. p # ba
9. Colinear(b;a;a')
10. p leftof a'b
11. B(baa')
12. a' leftof pb
⊢ False

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a' : Point
5. p : Point
6. p leftof ba
7. b # a'
8. p # ba
9. Colinear(b;a;a')
10. p leftof a'b
11. B(ba'a)
12. a' leftof pb
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -4
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  InstLemma  `left-convex`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}
  THEN  EAuto  2)

---

Home Index