---

Step * 1 1 of Lemma projective-points-exist


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)))
BY
{ ((RWO "geo-intersect-lines-iff" (-1) THENA Auto)
   THEN RepeatFor 3 (D -1)
   THEN RenameVar `p' (-3)
   THEN D 0 With ⌜inl p⌝ 
   THEN Auto
   THEN RepUR ``pp-sep`` 0
   THEN EAuto 1) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "geo-intersect-lines-iff"  (-1)  THENA  Auto)
  THEN  RepeatFor  3  (D  -1)
  THEN  RenameVar  `p'  (-3)
  THEN  D  0  With  \mkleeneopen{}inl  p\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``pp-sep``  0
  THEN  EAuto  1)

---

Home Index