---

Step * of Lemma proj-point-sep-iff-pp-sep

∀e:EuclideanParPlane
  ((∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n))))
  ⇒ (∀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 ((BLemma `proj-point-sep_defB` THEN Auto) ORELSE (BLemma `proj-point-sep_defA` THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((BLemma  `proj-point-sep\_defB`  THEN  Auto)  ORELSE  (BLemma  `proj-point-sep\_defA`  THEN  Auto))
  )

---

Home Index