---

Step * 4 2 1 of Lemma projective-points-exist


1. e : EuclideanParPlane
2. y : Unit
3. y1 : Unit
4. l : Line
⊢ ∃p:Point + Line. ((¬pp-sep(e;p;inr y )) ∧ (¬pp-sep(e;p;inr y1 )))
BY
{ (D 0 With ⌜inr l ⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  y  :  Unit
3.  y1  :  Unit
4.  l  :  Line
\mvdash{}  \mexists{}p:Point  +  Line.  ((\mneg{}pp-sep(e;p;inr  y  ))  \mwedge{}  (\mneg{}pp-sep(e;p;inr  y1  )))


By

---

Latex:
(D  0  With  \mkleeneopen{}inr  l  \mkleeneclose{}    THEN  Auto)

---

Home Index