---

Step * of Lemma geo-colinear-sep-cases

∀e:BasicGeometry. ∀a,b,c:Point.  (a ≠ b ⇒ Colinear(a;b;c) ⇒ ((¬((¬a_c_b) ∧ (¬a_b_c))) ∨ (¬((¬b_c_a) ∧ (¬b_a_c)))))
BY
{ ((Auto THEN (Assert a ≠ c ∨ b ≠ c BY Auto)) THEN D -1) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. Colinear(a;b;c)
7. a ≠ c
⊢ (¬((¬a_c_b) ∧ (¬a_b_c))) ∨ (¬((¬b_c_a) ∧ (¬b_a_c)))

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. Colinear(a;b;c)
7. b ≠ c
⊢ (¬((¬a_c_b) ∧ (¬a_b_c))) ∨ (¬((¬b_c_a) ∧ (¬b_a_c)))

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.
    (a  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  ((\mneg{}((\mneg{}a\_c\_b)  \mwedge{}  (\mneg{}a\_b\_c)))  \mvee{}  (\mneg{}((\mneg{}b\_c\_a)  \mwedge{}  (\mneg{}b\_a\_c)))))


By

---

Latex:
((Auto  THEN  (Assert  a  \mneq{}  c  \mvee{}  b  \mneq{}  c  BY  Auto))  THEN  D  -1)

---

Home Index