---

Step * 1 1 of Lemma geo-colinear-left-out3


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. x' : Point
9. Colinear(b;x;x')
10. a-x-c
11. a'-x'-c'
12. out(b aa')
13. out(b cc')
14. b leftof ac
15. b leftof a'c'
16. b leftof ax
17. b leftof a'x'
18. b # x'
19. ¬B(bxx')
20. ¬B(bx'x)
21. x'-b-x
22. a leftof xb ∧ x leftof ba
23. a' leftof x'b ∧ x' leftof ba'
⊢ False
BY
{ ((InstLemma `geo-colinear-left-out2` [⌜e⌝;⌜a'⌝;⌜b⌝;⌜x'⌝;⌜x⌝]⋅ THEN EAuto 1)
   THEN InstLemma `geo-left-out` [⌜e⌝;⌜a⌝;⌜b⌝;⌜a'⌝;⌜x⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  c'  :  Point
7.  x  :  Point
8.  x'  :  Point
9.  Colinear(b;x;x')
10.  a-x-c
11.  a'-x'-c'
12.  out(b  aa')
13.  out(b  cc')
14.  b  leftof  ac
15.  b  leftof  a'c'
16.  b  leftof  ax
17.  b  leftof  a'x'
18.  b  \#  x'
19.  \mneg{}B(bxx')
20.  \mneg{}B(bx'x)
21.  x'-b-x
22.  a  leftof  xb  \mwedge{}  x  leftof  ba
23.  a'  leftof  x'b  \mwedge{}  x'  leftof  ba'
\mvdash{}  False


By

---

Latex:
((InstLemma  `geo-colinear-left-out2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
  THEN  InstLemma  `geo-left-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index