---

Step * of Lemma eu-congruent-refl

∀e:EuclideanPlane. ∀[a,b:Point].  ab=ab
BY
{ (Auto THEN D 1 THEN (Unhide THENA Auto) THEN D 2 THEN ExRepD THEN InstHyp [⌜b⌝;⌜a⌝;⌜a⌝;⌜b⌝;⌜a⌝;⌜b⌝] 3⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b:Point].    ab=ab


By

---

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

---

Home Index