---

Step * 1 2 of Lemma proj-point-sep_defA


1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. ∃m:Line. (x I m ∧ x1 # m)
⊢ ∃n:Line?. ((¬pp-sep(e;inl x;n)) ∧ pp-sep(e;inl x1;n))
BY
{ (RepeatFor 2 (D -1) THEN D 0 With ⌜inl m⌝  THEN Auto THEN RepUR ``pp-sep`` 0 THEN (D 0 THENA Auto)) }

1
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. m : Line
6. x I m
7. x1 # m
8. x # m
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  D  0  With  \mkleeneopen{}inl  m\mkleeneclose{}    THEN  Auto  THEN  RepUR  ``pp-sep``  0  THEN  (D  0  THENA  Auto))

---

Home Index