---

Step * of Lemma geo-intersect-LINE-iff-line

No Annotations
∀eu:EuclideanParPlane. ∀L,M:LINE.  (L \/ M ⇐⇒ ∃l:{l:Line| l = L ∈ LINE} . ∃m:{m:Line| m = M ∈ LINE} . l \/ m)
BY
{ Auto }

1
1. eu : EuclideanParPlane
2. L : LINE
3. M : LINE
4. L \/ M
⊢ ∃l:{l:Line| l = L ∈ LINE} . ∃m:{m:Line| m = M ∈ LINE} . l \/ m

2
1. eu : EuclideanParPlane
2. L : LINE
3. M : LINE
4. ∃l:{l:Line| l = L ∈ LINE} . ∃m:{m:Line| m = M ∈ LINE} . l \/ m
⊢ L \/ M

---

Latex:

---

Latex:
No  Annotations
\mforall{}eu:EuclideanParPlane.  \mforall{}L,M:LINE.    (L  \mbackslash{}/  M  \mLeftarrow{}{}\mRightarrow{}  \mexists{}l:\{l:Line|  l  =  L\}  .  \mexists{}m:\{m:Line|  m  =  M\}  .  l  \mbackslash{}/  m)


By

---

Latex:
Auto

---

Home Index