---

Step * of Lemma geo-intersect-all-parallel2

∀e:EuclideanPlane. ∀L,M,N:Line.  ((L \/ N ∧ (∀l,m:LINE.  (l \/ m ⇒ (∀n:LINE. (l \/ n ∨ m \/ n))))) ⇒ L || M ⇒ M \/ N)
BY
{ Auto }

1
1. e : EuclideanPlane
2. L : Line
3. M : Line
4. N : Line
5. L \/ N
6. ∀l,m:LINE.  (l \/ m ⇒ (∀n:LINE. (l \/ n ∨ m \/ n)))
7. L || M
⊢ M \/ N

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}L,M,N:Line.
    ((L  \mbackslash{}/  N  \mwedge{}  (\mforall{}l,m:LINE.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (\mforall{}n:LINE.  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n)))))  {}\mRightarrow{}  L  ||  M  {}\mRightarrow{}  M  \mbackslash{}/  N)


By

---

Latex:
Auto

---

Home Index