---

Step * 1 of Lemma projective-points-exist


1. e : EuclideanParPlane
2. x : Line
3. x1 : Line
⊢ ¬¬(∃p:Point + Line. ((¬pp-sep(e;p;inl x)) ∧ (¬pp-sep(e;p;inl x1))))
BY
{ ((StableCases ⌜x \/ x1⌝⋅ THENA Auto) THEN (RemoveDoubleNegation THENA Auto)) }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((StableCases  \mkleeneopen{}x  \mbackslash{}/  x1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (RemoveDoubleNegation  THENA  Auto))

---

Home Index