---

Step * of Lemma qeq-qrep

∀[r:ℚ]. qeq(r;qrep(r)) = tt
BY
{ xxxxxx((D 0 THENA Auto) THEN D (-1)⋅ THEN Auto THEN (GenConclTerm ⌜r⌝ ⋅ THENA Auto) THEN All Thin)xxxxxx }

1
1. v : ℤ ⋃ (ℤ × ℤ-o)
⊢ qeq(v;qrep(v)) = tt

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  qeq(r;qrep(r))  =  tt


By

---

Latex:
xxxxxx((D  0  THENA  Auto)
              THEN  D  (-1)\mcdot{}
              THEN  Auto
              THEN  (GenConclTerm  \mkleeneopen{}r\mkleeneclose{}  \mcdot{}  THENA  Auto)
              THEN  All  Thin)xxxxxx

---

Home Index