---

Step * of Lemma proj-point-sep_defA

∀e:EuclideanParPlane. ∀p,q:Point + Line.  (proj-point-sep(e;p;q) ⇒ (∃n:Line?. ((¬pp-sep(e;p;n)) ∧ pp-sep(e;q;n))))
BY
{ (((Auto THEN DVar `p' THEN DVar `q') THEN Unfold `proj-point-sep` -1) THEN All Reduce⋅) }

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

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

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

4
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))

---

Latex:

---

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


By

---

Latex:
(((Auto  THEN  DVar  `p'  THEN  DVar  `q')  THEN  Unfold  `proj-point-sep`  -1)  THEN  All  Reduce\mcdot{})

---

Home Index