---

Step * of Lemma projective-lines-exist

∀e:EuclideanParPlane. ∀p1,p2:Point + Line.
  (proj-point-sep(e;p1;p2) ⇒ (∃l:Line?. ((¬pp-sep(e;p1;l)) ∧ (¬pp-sep(e;p2;l)))))
BY
{ (Auto THEN DVar `p1' THEN DVar `p2' THEN RepUR ``proj-point-sep`` -1) }

1
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
⊢ ∃l:Line?. ((¬pp-sep(e;inl x;l)) ∧ (¬pp-sep(e;inl x1;l)))

2
1. e : EuclideanParPlane
2. x : Point
3. y : Line
4. True
⊢ ∃l:Line?. ((¬pp-sep(e;inl x;l)) ∧ (¬pp-sep(e;inr y ;l)))

3
1. e : EuclideanParPlane
2. y : Line
3. x : Point
4. True
⊢ ∃l:Line?. ((¬pp-sep(e;inr y ;l)) ∧ (¬pp-sep(e;inl x;l)))

4
1. e : EuclideanParPlane
2. y : Line
3. y1 : Line
4. y \/ y1
⊢ ∃l:Line?. ((¬pp-sep(e;inr y ;l)) ∧ (¬pp-sep(e;inr y1 ;l)))

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}p1,p2:Point  +  Line.
    (proj-point-sep(e;p1;p2)  {}\mRightarrow{}  (\mexists{}l:Line?.  ((\mneg{}pp-sep(e;p1;l))  \mwedge{}  (\mneg{}pp-sep(e;p2;l)))))


By

---

Latex:
(Auto  THEN  DVar  `p1'  THEN  DVar  `p2'  THEN  RepUR  ``proj-point-sep``  -1)

---

Home Index