---

Step * 3 of Lemma projective-points-exist


1. e : EuclideanParPlane
2. y : Unit
3. x : Line
⊢ ¬¬(∃p:Point + Line. ((¬pp-sep(e;p;inr y )) ∧ (¬pp-sep(e;p;inl x))))
BY
{ ((RemoveDoubleNegation THENA Auto) THEN D 0 With ⌜inr x ⌝  THEN Auto THEN RepUR ``pp-sep`` 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index