---

Step * of Lemma canonical-parallel2

∀e:EuclideanParPlane. ∀c:l,m:Line//l || m. ∀a:Point.  (∃l:{l:LINE| a I l}  [(l = c ∈ (l,m:Line//l || m))])
BY
{ (Auto THEN Assert ⌜∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])⌝⋅) }

1
.....assertion..... 
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
3. a : Point
⊢ ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])

2
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
3. a : Point
4. ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
⊢ ∃l:{l:LINE| a I l}  [(l = c ∈ (l,m:Line//l || m))]

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}p:Point.  \mforall{}l:Line.    (\mexists{}m:Line  [(l  ||  m  \mwedge{}  p  I  m)])\mkleeneclose{}\mcdot{})

---

Home Index