---

Step * of Lemma eu-congruent-comm

∀e:EuclideanPlane. ∀[a,b,c,d:Point].  ba=dc supposing ab=cd
BY
{ (Auto THEN (FLemma `eu-congruent-left-comm` [-1]⋅ THEN Auto) THEN FLemma `eu-congruent-right-comm` [-1]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c,d:Point].    ba=dc  supposing  ab=cd


By

---

Latex:
(Auto
  THEN  (FLemma  `eu-congruent-left-comm`  [-1]\mcdot{}  THEN  Auto)
  THEN  FLemma  `eu-congruent-right-comm`  [-1]\mcdot{}
  THEN  Auto)

---

Home Index