---

Step * of Lemma canonical-parallel

∀e:EuclideanParPlane. ∀c:l,m:Line//l || m.  (∃l:LINE [(l = c ∈ (l,m:Line//l || m))])
BY
{ Auto }

1
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
⊢ ∃l:LINE [(l = c ∈ (l,m:Line//l || m))]

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}c:l,m:Line//l  ||  m.    (\mexists{}l:LINE  [(l  =  c)])


By

---

Latex:
Auto

---

Home Index