---

Step * of Lemma eu-colinear-cases

∀e:EuclideanStructure
  ∀[a,b,c:Point].
    ∀X:ℙ
      (Stable{X}
      ⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point)) ⇒ X)
      ⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point)) ⇒ X)
      ⇒ (((¬(a = b ∈ Point)) ∧ c-a-b) ⇒ X)
      ⇒ (((¬(a = b ∈ Point)) ∧ a-c-b) ⇒ X)
      ⇒ (((¬(a = b ∈ Point)) ∧ a-b-c) ⇒ X)
      ⇒ ((¬Colinear(a;b;c)) ⇒ X)
      ⇒ X)
BY
{ (Auto THEN (D 6 THEN Auto) THEN (D 0 THENA Auto)) }

1
1. e : EuclideanStructure@i'
2. a : Point
3. b : Point
4. c : Point
5. X : ℙ@i'
6. ((¬(a = b ∈ Point)) ∧ (c = a ∈ Point)) ⇒ X@i
7. ((¬(a = b ∈ Point)) ∧ (c = b ∈ Point)) ⇒ X@i
8. ((¬(a = b ∈ Point)) ∧ c-a-b) ⇒ X@i
9. ((¬(a = b ∈ Point)) ∧ a-c-b) ⇒ X@i
10. ((¬(a = b ∈ Point)) ∧ a-b-c) ⇒ X@i
11. (¬Colinear(a;b;c)) ⇒ X@i
12. ¬X@i
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (D  6  THEN  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index