---

Step * of Lemma geo-out-iff-colinear

∀e:BasicGeometry. ∀p,a,b:Point.  (out(p ab) ⇐⇒ (Colinear(p;a;b) ∧ (¬a_p_b)) ∧ p ≠ a ∧ p ≠ b)
BY
{ Auto }

1
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. out(p ab)
⊢ ¬a_p_b

2
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. Colinear(p;a;b)
6. ¬a_p_b
7. p ≠ a
8. p ≠ b
⊢ out(p ab)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,a,b:Point.    (out(p  ab)  \mLeftarrow{}{}\mRightarrow{}  (Colinear(p;a;b)  \mwedge{}  (\mneg{}a\_p\_b))  \mwedge{}  p  \mneq{}  a  \mwedge{}  p  \mneq{}  b)


By

---

Latex:
Auto

---

Home Index