---

Step * 2 1 2 2 of Lemma canonical-parallel2

.....set predicate..... 
1. e : EuclideanParPlane
2. c : l,m:Line//l || m
3. a : Point
4. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
5. f a c ∈ {l:LINE| a I l} 
⊢ (f a c) = c ∈ (l,m:Line//l || m)
BY
{ (D 2 THEN EqTypeCD THEN Auto) }

1
.....antecedent..... 
1. e : EuclideanParPlane
2. c : Base
3. c1 : Base
4. c = c1 ∈ pertype(λl,m. ((l ∈ Line) ∧ (m ∈ Line) ∧ l || m))
5. c ∈ Line
6. c1 ∈ Line
7. c || c1
8. a : Point
9. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
10. f a c ∈ {l:LINE| a I l} 
⊢ f a c || c1

---

Latex:

---

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


By

---

Latex:
(D  2  THEN  EqTypeCD  THEN  Auto)

---

Home Index