---

Step * 1 of Lemma int_ring_wf


ℤ-rng ∈ CRng
BY
{ MemTypeCD }

1
ℤ-rng ∈ Rng

2
.....set predicate..... 
Comm(|ℤ-rng|;*)

3
.....wf..... 
1. r : Rng
⊢ Comm(|r|;*) ∈ Type

---

Latex:

---

Latex:

\mBbbZ{}-rng  \mmember{}  CRng


By

---

Latex:
MemTypeCD

---

Home Index