---

Step * 1 2 1 1 1 of Lemma canonical-parallel


1. e : EuclideanParPlane
2. c : Base
3. c1 : Base
4. c = c1 ∈ (l,m:Line//l || m)
5. c ∈ Line
6. c1 ∈ Line
7. c || c1
8. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
⊢ (f O c) = (f O c1) ∈ LINE
BY
{ (GenConclTerms Auto [⌜f O c⌝;⌜f O c1⌝]⋅
   THEN Thin (-1)
   THEN Thin (-2)
   THEN RepeatFor 2 (D -2)
   THEN RepeatFor 2 (D -1)) }

1
1. e : EuclideanParPlane
2. c : Base
3. c1 : Base
4. c = c1 ∈ (l,m:Line//l || m)
5. c ∈ Line
6. c1 ∈ Line
7. c || c1
8. f : ∀p:Point. ∀l:Line.  (∃m:Line [(l || m ∧ p I m)])
9. v : Line
10. c || v
11. O I v
12. v1 : Line
13. c1 || v1
14. O I v1
⊢ v = v1 ∈ LINE

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  c  :  Base
3.  c1  :  Base
4.  c  =  c1
5.  c  \mmember{}  Line
6.  c1  \mmember{}  Line
7.  c  ||  c1
8.  f  :  \mforall{}p:Point.  \mforall{}l:Line.    (\mexists{}m:Line  [(l  ||  m  \mwedge{}  p  I  m)])
\mvdash{}  (f  O  c)  =  (f  O  c1)


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}f  O  c\mkleeneclose{};\mkleeneopen{}f  O  c1\mkleeneclose{}]\mcdot{}
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  RepeatFor  2  (D  -2)
  THEN  RepeatFor  2  (D  -1))

---

Home Index