---

Step * of Lemma proj-point-sep-cotrans

∀e:EuclideanParPlane
  ((∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n))))
  ⇒ (∀x,y:Point + Line.
        (proj-point-sep(e;x;y) ⇒ (∀z:Point + Line. (proj-point-sep(e;x;z) ∨ proj-point-sep(e;y;z))))))
BY
{ (Auto THEN DVar `x' THEN DVar `y' THEN DVar `z' THEN All (RepUR ``proj-point-sep``) 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{}x,y:Point  +  Line.
                (proj-point-sep(e;x;y)
                {}\mRightarrow{}  (\mforall{}z:Point  +  Line.  (proj-point-sep(e;x;z)  \mvee{}  proj-point-sep(e;y;z))))))


By

---

Latex:
(Auto  THEN  DVar  `x'  THEN  DVar  `y'  THEN  DVar  `z'  THEN  All  (RepUR  ``proj-point-sep``)  THEN  Auto)

---

Home Index