---

Step * of Lemma geo-colinear-not-out

No Annotations
∀e:BasicGeometry. ∀a,b,c:Point.  (Colinear(a;b;c) ⇒ (¬out(a bc) ⇐⇒ B(bac)))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Colinear(a;b;c)
6. ¬out(a bc)
⊢ B(bac)

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Colinear(a;b;c)
6. B(bac)
⊢ ¬out(a bc)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (Colinear(a;b;c)  {}\mRightarrow{}  (\mneg{}out(a  bc)  \mLeftarrow{}{}\mRightarrow{}  B(bac)))


By

---

Latex:
Auto

---

Home Index