---

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


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. v : Line
11. c || v
12. a I v
13. v1 : Line
14. c1 || v1
15. a I v1
⊢ v = v1 ∈ {l:LINE| a I l} 
BY
{ ((InstLemma `geo-playfair-axiom` [⌜e⌝]⋅ THEN Auto) THEN InstHyp [⌜a⌝;⌜c⌝;⌜v⌝;⌜v1⌝] (-1)⋅ THEN Try (Complete (Auto))) }

---

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.  a  :  Point
9.  f  :  \mforall{}p:Point.  \mforall{}l:Line.    (\mexists{}m:Line  [(l  ||  m  \mwedge{}  p  I  m)])
10.  v  :  Line
11.  c  ||  v
12.  a  I  v
13.  v1  :  Line
14.  c1  ||  v1
15.  a  I  v1
\mvdash{}  v  =  v1


By

---

Latex:
((InstLemma  `geo-playfair-axiom`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index