---

Step * of Lemma p_inf-l_eu-sep-exists

∀eu:EuclideanParPlane. ∀p:l,m:Line//l || m. ∀m:Line.  ((m = p ∈ (l,m:Line//l || m)) ⇒ (∃L:Line. (¬m || L)))
BY
{ Auto }

1
1. eu : EuclideanParPlane
2. p : l,m:Line//l || m
3. m : Line
4. m = p ∈ (l,m:Line//l || m)
⊢ ∃L:Line. (¬m || L)

---

Latex:

---

Latex:
\mforall{}eu:EuclideanParPlane.  \mforall{}p:l,m:Line//l  ||  m.  \mforall{}m:Line.    ((m  =  p)  {}\mRightarrow{}  (\mexists{}L:Line.  (\mneg{}m  ||  L)))


By

---

Latex:
Auto

---

Home Index