---

Step * 3 of Lemma projective-lines-exist


1. e : EuclideanParPlane
2. y : Line
3. x : Point
4. True
⊢ ∃l:Line?. ((¬pp-sep(e;inr y ;l)) ∧ (¬pp-sep(e;inl x;l)))
BY
{ (((InstLemma `Euclid-parallel-exists` [⌜e⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto) THEN ExRepD)
   THEN (D 0 With ⌜inl m⌝  THENA Auto)
   THEN RepUR ``pp-sep`` 0
   THEN Fold `geo-Aparallel` 0
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  y  :  Line
3.  x  :  Point
4.  True
\mvdash{}  \mexists{}l:Line?.  ((\mneg{}pp-sep(e;inr  y  ;l))  \mwedge{}  (\mneg{}pp-sep(e;inl  x;l)))


By

---

Latex:
(((InstLemma  `Euclid-parallel-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (D  0  With  \mkleeneopen{}inl  m\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``pp-sep``  0
  THEN  Fold  `geo-Aparallel`  0
  THEN  EAuto  1)

---

Home Index