---

Step * 1 of Lemma projective-lines-exist


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)))
BY
{ (RenameVar `sep' (-1)
   THEN D 0 With ⌜inl <x, x1, sep>⌝ 
   THEN Auto
   THEN RepUR ``pp-sep`` 0
   THEN RepUR ``geo-plsep`` 0
   THEN RWO "not-lsep-iff-colinear" 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `sep'  (-1)
  THEN  D  0  With  \mkleeneopen{}inl  <x,  x1,  sep>\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``pp-sep``  0
  THEN  RepUR  ``geo-plsep``  0
  THEN  RWO  "not-lsep-iff-colinear"  0
  THEN  Auto)

---

Home Index