---

Step * of Lemma proj-point-sep-irrefl

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

---

Latex:

---

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


By

---

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

---

Home Index