---

Step * of Lemma proj-line-sep-irrefl

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

1
1. e : EuclideanParPlane
2. x1 : Line
⊢ ¬geo-line-sep(e;x1;x1)

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}x:Line?.    (\mneg{}proj-line-sep(e;x;x))


By

---

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

---

Home Index