---

Step * of Lemma geo-congruent-comm

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

---

Latex:

---

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


By

---

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

---

Home Index