---

Step * 4 of Lemma projective-lines-exist


1. e : EuclideanParPlane
2. y : Line
3. y1 : Line
4. y \/ y1
⊢ ∃l:Line?. ((¬pp-sep(e;inr y ;l)) ∧ (¬pp-sep(e;inr y1 ;l)))
BY
{ ((D 0 With ⌜inr ⋅ ⌝  THENA Auto) THEN RepUR ``pp-sep`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  y  :  Line
3.  y1  :  Line
4.  y  \mbackslash{}/  y1
\mvdash{}  \mexists{}l:Line?.  ((\mneg{}pp-sep(e;inr  y  ;l))  \mwedge{}  (\mneg{}pp-sep(e;inr  y1  ;l)))


By

---

Latex:
((D  0  With  \mkleeneopen{}inr  \mcdot{}  \mkleeneclose{}    THENA  Auto)  THEN  RepUR  ``pp-sep``  0  THEN  Auto)

---

Home Index