---

Step * 1 of Lemma eu-congruent-left-comm


1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [d] : Point
6. [%] : ab=cd
7. e ∈ EuclideanPlane
⊢ ba=cd
BY
{ (D 1 THEN (Unhide THENA Auto) THEN D 2 THEN ExRepD THEN InstHyp [⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜b⌝] 3⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  [a]  :  Point
3.  [b]  :  Point
4.  [c]  :  Point
5.  [d]  :  Point
6.  [\%]  :  ab=cd
7.  e  \mmember{}  EuclideanPlane
\mvdash{}  ba=cd


By

---

Latex:
(D  1
  THEN  (Unhide  THENA  Auto)
  THEN  D  2
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  3\mcdot{}
  THEN  Auto)

---

Home Index