---

Step * 4 of Lemma proj-point-sep_defA


1. e : EuclideanParPlane
2. y : Line
3. y1 : Line
4. y \/ y1
⊢ ∃n:Line?. ((¬pp-sep(e;inr y ;n)) ∧ pp-sep(e;inr y1 ;n))
BY
{ ((D 0 With ⌜inl y⌝  THEN Auto) THEN Unfold `pp-sep` 0 THEN All Reduce⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  y  :  Line
3.  y1  :  Line
4.  y  \mbackslash{}/  y1
\mvdash{}  \mexists{}n:Line?.  ((\mneg{}pp-sep(e;inr  y  ;n))  \mwedge{}  pp-sep(e;inr  y1  ;n))


By

---

Latex:
((D  0  With  \mkleeneopen{}inl  y\mkleeneclose{}    THEN  Auto)  THEN  Unfold  `pp-sep`  0  THEN  All  Reduce\mcdot{}  THEN  EAuto  1)

---

Home Index