---

Step * of Lemma geo-colinear-cases

∀e:BasicGeometry-
  ∀[a,b,c:Point].
    ∀X:ℙ
      (Stable{X}
      ⇒ (a ≡ b ⇒ X)
      ⇒ (b ≡ c ⇒ X)
      ⇒ (c ≡ a ⇒ X)
      ⇒ (a-b-c ⇒ X)
      ⇒ (b-c-a ⇒ X)
      ⇒ (c-a-b ⇒ X)
      ⇒ ((¬Colinear(a;b;c)) ⇒ X)
      ⇒ X)
BY
{ (InstLemma `geo-simple-colinear-cases` []
   THEN RepeatFor 6 (ParallelLast')
   THEN Auto
   THEN BackThruHyp' 6
   THEN (D 0 THENA Auto)
   THEN DistinguishCases ⌜Colinear(a;b;c)⌝⋅
   THEN Auto) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. X : ℙ
6. X supposing ¬¬X
7. a ≡ b ⇒ X
8. b ≡ c ⇒ X
9. c ≡ a ⇒ X
10. a-b-c ⇒ X
11. b-c-a ⇒ X
12. c-a-b ⇒ X
13. (¬Colinear(a;b;c)) ⇒ X
14. ¬X
15. Colinear(a;b;c)
16. (a_b_c ⇒ X) ⇒ (b_c_a ⇒ X) ⇒ (c_a_b ⇒ X) ⇒ X
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry-
    \mforall{}[a,b,c:Point].
        \mforall{}X:\mBbbP{}
            (Stable\{X\}
            {}\mRightarrow{}  (a  \mequiv{}  b  {}\mRightarrow{}  X)
            {}\mRightarrow{}  (b  \mequiv{}  c  {}\mRightarrow{}  X)
            {}\mRightarrow{}  (c  \mequiv{}  a  {}\mRightarrow{}  X)
            {}\mRightarrow{}  (a-b-c  {}\mRightarrow{}  X)
            {}\mRightarrow{}  (b-c-a  {}\mRightarrow{}  X)
            {}\mRightarrow{}  (c-a-b  {}\mRightarrow{}  X)
            {}\mRightarrow{}  ((\mneg{}Colinear(a;b;c))  {}\mRightarrow{}  X)
            {}\mRightarrow{}  X)


By

---

Latex:
(InstLemma  `geo-simple-colinear-cases`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Auto
  THEN  BackThruHyp'  6
  THEN  (D  0  THENA  Auto)
  THEN  DistinguishCases  \mkleeneopen{}Colinear(a;b;c)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index