---

Step * of Lemma geo-colinear-iff

No Annotations
∀e:BasicGeometry-. ∀a,b,c:Point.  (Colinear(a;b;c) ⇐⇒ ¬((¬B(abc)) ∧ (¬B(bca)) ∧ (¬B(cab))))
BY
{ Auto }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. Colinear(a;b;c)
⊢ ¬((¬B(abc)) ∧ (¬B(bca)) ∧ (¬B(cab)))

2
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. ¬((¬B(abc)) ∧ (¬B(bca)) ∧ (¬B(cab)))
⊢ Colinear(a;b;c)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry-.  \mforall{}a,b,c:Point.    (Colinear(a;b;c)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((\mneg{}B(abc))  \mwedge{}  (\mneg{}B(bca))  \mwedge{}  (\mneg{}B(cab))))


By

---

Latex:
Auto

---

Home Index