---

Step * of Lemma geo-simple-colinear-cases

∀[e:BasicGeometry-]. ∀[a,b,c:Point].
  ∀X:ℙ. (Stable{X} ⇒ Colinear(a;b;c) ⇒ (a_b_c ⇒ X) ⇒ (b_c_a ⇒ X) ⇒ (c_a_b ⇒ X) ⇒ X)
BY
{ (Auto THEN BackThruHyp' 6) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BackThruHyp'  6)

---

Home Index