---

Step * of Lemma qeq-equiv

EquivRel(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
BY
{ (D 0 THEN Auto THEN First [BLemma `qeq-refl`; BLemma `qeq-sym`; BLemma `qeq-trans`]) }

---

Latex:

---

Latex:
EquivRel(\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{});r,s.qeq(r;s)  =  tt)


By

---

Latex:
(D  0  THEN  Auto  THEN  First  [BLemma  `qeq-refl`;  BLemma  `qeq-sym`;  BLemma  `qeq-trans`])

---

Home Index