---

Step * of Lemma proj-point-sep-symmetry

∀e:EuclideanParPlane. ∀x,y:Point + Line.  (proj-point-sep(e;x;y) ⇒ proj-point-sep(e;y;x))
BY
{ (Auto THEN DVar `x' THEN DVar `y' THEN All (RepUR ``proj-point-sep``) THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}x,y:Point  +  Line.    (proj-point-sep(e;x;y)  {}\mRightarrow{}  proj-point-sep(e;y;x))


By

---

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

---

Home Index