---

Step * 1 of Lemma canonical-parallel2

.....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)])
BY
{ (Auto THEN InstLemma `Euclid-parallel-exists` [⌜e⌝;⌜l⌝;⌜p⌝]⋅ THEN Auto THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanParPlane
2.  c  :  l,m:Line//l  ||  m
3.  a  :  Point
\mvdash{}  \mforall{}p:Point.  \mforall{}l:Line.    (\mexists{}m:Line  [(l  ||  m  \mwedge{}  p  I  m)])


By

---

Latex:
(Auto  THEN  InstLemma  `Euclid-parallel-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  ParallelLast  THEN  Auto)

---

Home Index