---

Step * 1 of Lemma eu-congruent-transitivity


1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [d] : Point
6. [x] : Point
7. [y] : Point
8. [%] : ab=cd
9. [%1] : cd=xy
10. e ∈ EuclideanPlane
⊢ ab=xy
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.  [x]  :  Point
7.  [y]  :  Point
8.  [\%]  :  ab=cd
9.  [\%1]  :  cd=xy
10.  e  \mmember{}  EuclideanPlane
\mvdash{}  ab=xy


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