---

Step * of Lemma eu-congruent-left-comm

∀e:EuclideanPlane. ∀[a,b,c,d:Point].  ba=cd supposing ab=cd
BY
{ (Auto THEN (Assert e ∈ EuclideanPlane BY Auto)) }

1
1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [d] : Point
6. [%] : ab=cd
7. e ∈ EuclideanPlane
⊢ ba=cd

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (Assert  e  \mmember{}  EuclideanPlane  BY  Auto))

---

Home Index