---

Step * of Lemma geo-out-iff-exists

∀e:BasicGeometry. ∀p,a,b:Point.  (out(p ab) ⇐⇒ (∃c:Point. (p ≠ c ∧ a_p_c ∧ b_p_c)) ∧ p ≠ a ∧ p ≠ b)
BY
{ Auto }

1
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. out(p ab)
⊢ ∃c:Point. (p ≠ c ∧ a_p_c ∧ b_p_c)

2
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. ∃c:Point. (p ≠ c ∧ a_p_c ∧ b_p_c)
6. p ≠ a
7. p ≠ b
⊢ out(p ab)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,a,b:Point.    (out(p  ab)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}c:Point.  (p  \mneq{}  c  \mwedge{}  a\_p\_c  \mwedge{}  b\_p\_c))  \mwedge{}  p  \mneq{}  a  \mwedge{}  p  \mneq{}  b)


By

---

Latex:
Auto

---

Home Index