---

Step * 1 2 1 2 of Lemma canonical-parallel


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

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

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

3
.....wf..... 
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
3. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
4. f O c ∈ LINE
5. l : LINE
⊢ istype(l = c ∈ (l,m:Line//l || m))

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  c  :  l,m:Line//l  ||  m
3.  f  :  \mforall{}p:Point.  \mforall{}l:Line.    (\mexists{}m:Line  [(l  ||  m  \mwedge{}  p  I  m)])
4.  f  O  c  \mmember{}  LINE
\mvdash{}  f  O  c  \mmember{}  \mexists{}l:LINE  [(l  =  c)]


By

---

Latex:
MemTypeCD

---

Home Index