---

Step * of Lemma projective-points-exist

∀e:EuclideanParPlane. ∀l,m:Line?.  (¬¬(∃p:Point + Line. ((¬pp-sep(e;p;l)) ∧ (¬pp-sep(e;p;m)))))
BY
{ (Auto THEN DVar `l' THEN DVar `m') }

1
1. e : EuclideanParPlane
2. x : Line
3. x1 : Line
⊢ ¬¬(∃p:Point + Line. ((¬pp-sep(e;p;inl x)) ∧ (¬pp-sep(e;p;inl x1))))

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

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

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

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}l,m:Line?.    (\mneg{}\mneg{}(\mexists{}p:Point  +  Line.  ((\mneg{}pp-sep(e;p;l))  \mwedge{}  (\mneg{}pp-sep(e;p;m)))))


By

---

Latex:
(Auto  THEN  DVar  `l'  THEN  DVar  `m')

---

Home Index