---

Step * of Lemma geo-eq_inversion

∀[e:EuclideanPlane]. ∀[a,b:Point].  a ≡ b supposing b ≡ a
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  EAuto  1)

---

Home Index