---

Step * 4 of Lemma projective-points-exist


1. e : EuclideanParPlane
2. y : Unit
3. y1 : Unit
⊢ ¬¬(∃p:Point + Line. ((¬pp-sep(e;p;inr y )) ∧ (¬pp-sep(e;p;inr y1 ))))
BY
{ Assert ⌜Line⌝⋅ }

1
.....assertion..... 
1. e : EuclideanParPlane
2. y : Unit
3. y1 : Unit
⊢ Line

2
1. e : EuclideanParPlane
2. y : Unit
3. y1 : Unit
4. Line
⊢ ¬¬(∃p:Point + Line. ((¬pp-sep(e;p;inr y )) ∧ (¬pp-sep(e;p;inr y1 ))))

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}Line\mkleeneclose{}\mcdot{}

---

Home Index