---

Step * of Lemma qeq-wf

∀[r,s:ℚ].  (qeq(r;s) ∈ 𝔹)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (D 2 THENA Auto) THEN (D 1 THENA Auto)) }

1
1. r : Base
2. r1 : Base
3. r = r1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
4. r ∈ ℤ ⋃ (ℤ × ℤ-o)
5. r1 ∈ ℤ ⋃ (ℤ × ℤ-o)
6. qeq(r;r1) = tt
7. s : Base
8. s1 : Base
9. s = s1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
10. s ∈ ℤ ⋃ (ℤ × ℤ-o)
11. s1 ∈ ℤ ⋃ (ℤ × ℤ-o)
12. qeq(s;s1) = tt
⊢ qeq(r;s) = qeq(r1;s1)

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbQ{}].    (qeq(r;s)  \mmember{}  \mBbbB{})


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  (D  2  THENA  Auto)  THEN  (D  1  THENA  Auto))

---

Home Index