---

Step * of Lemma geo-not-colinear

No Annotations
∀e:BasicGeometry. ∀[a,b,c:Point].  (¬Colinear(a;b;c) ⇐⇒ ¬(B(abc) ∨ B(bca) ∨ B(cab)))
BY
{ (Auto THEN Try ((Unfold `geo-colinear` -1 THEN (SupposeMore (-1) THENA Auto)))) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
⊢ ¬(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].    (\mneg{}Colinear(a;b;c)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(B(abc)  \mvee{}  B(bca)  \mvee{}  B(cab)))


By

---

Latex:
(Auto  THEN  Try  ((Unfold  `geo-colinear`  -1  THEN  (SupposeMore  (-1)  THENA  Auto))))

---

Home Index