---

Step * of Lemma proj-point-sep_defB

∀e:EuclideanParPlane. ∀p,q:Point + Line.
  (((∃n:Line?. ((¬pp-sep(e;p;n)) ∧ pp-sep(e;q;n))) ∧ (∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))))
  ⇒ proj-point-sep(e;p;q))
BY
{ ((Auto THEN ExRepD)
   THEN (DVar `n' THEN DVar `p' THEN DVar `q')
   THEN ((Unfold `pp-sep` -3 THEN Unfold `pp-sep` -2) THEN Unfold `proj-point-sep` 0)
   THEN All Reduce⋅
   THEN Auto) }

1
1. e : EuclideanParPlane
2. x1 : Point
3. x2 : Point
4. x : Line
5. ¬x1 # x
6. x2 # x
7. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
⊢ x1 ≠ x2

2
1. e : EuclideanParPlane
2. y : Line
3. y1 : Line
4. x : Line
5. ¬y \/ x
6. y1 \/ x
7. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
⊢ y \/ y1

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  ExRepD)
  THEN  (DVar  `n'  THEN  DVar  `p'  THEN  DVar  `q')
  THEN  ((Unfold  `pp-sep`  -3  THEN  Unfold  `pp-sep`  -2)  THEN  Unfold  `proj-point-sep`  0)
  THEN  All  Reduce\mcdot{}
  THEN  Auto)

---

Home Index