---

Step * of Lemma rationals_wf

ℚ ∈ Type
BY
{ Unfold `rationals` 0
THEN BLemma `quotient_wf`
THEN Try (BLemma `qeq-equiv`)
THEN Auto }

---

Latex:

---

Latex:
\mBbbQ{}  \mmember{}  Type


By

---

Latex:
Unfold  `rationals`  0
THEN  BLemma  `quotient\_wf`
THEN  Try  (BLemma  `qeq-equiv`)
THEN  Auto

---

Home Index