---

Step * of Lemma geo-colinear-left-out3

No Annotations
∀e:EuclideanPlane. ∀a,b,c,a',c',x,x':Point.
  (Colinear(b;x;x') ⇒ a-x-c ⇒ a'-x'-c' ⇒ out(b aa') ⇒ out(b cc') ⇒ b leftof ac ⇒ b leftof a'c' ⇒ out(b xx'))
BY
{ (Auto
   THEN (InstLemma `between-preserves-left-2` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜x⌝]⋅ THENA Auto)
   THEN (InstLemma `between-preserves-left-2` [⌜e⌝;⌜a'⌝;⌜c'⌝;⌜b⌝;⌜x'⌝]⋅ THENA Auto)
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN gColinearCases (9)
   THEN Auto) }

1
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
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,a',c',x,x':Point.
    (Colinear(b;x;x')
    {}\mRightarrow{}  a-x-c
    {}\mRightarrow{}  a'-x'-c'
    {}\mRightarrow{}  out(b  aa')
    {}\mRightarrow{}  out(b  cc')
    {}\mRightarrow{}  b  leftof  ac
    {}\mRightarrow{}  b  leftof  a'c'
    {}\mRightarrow{}  out(b  xx'))


By

---

Latex:
(Auto
  THEN  (InstLemma  `between-preserves-left-2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `between-preserves-left-2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  gColinearCases  (9)
  THEN  Auto)

---

Home Index