---

Step * 4 2 of Lemma projective-points-exist


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 ))))
BY
{ (RenameVar `l' (-1) THEN (RemoveDoubleNegation THENA Auto)) }

1
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 )))

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `l'  (-1)  THEN  (RemoveDoubleNegation  THENA  Auto))

---

Home Index