---

Step * of Lemma geo-sep-irrefl

∀e:EuclideanPlane. ∀[a,b:Point].  ¬a ≠ b supposing a = b ∈ Point
BY
{ (Auto THEN Fold `geo-eq` 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b:Point].    \mneg{}a  \mneq{}  b  supposing  a  =  b


By

---

Latex:
(Auto  THEN  Fold  `geo-eq`  0  THEN  EAuto  1)

---

Home Index