---

Step * 1 1 of Lemma int_ring_wf


ℤ-rng ∈ Rng
BY
{ MemTypeCD }

1
ℤ-rng ∈ RngSig

2
.....set predicate..... 
IsRing(|ℤ-rng|;+ℤ-rng;0;-ℤ-rng;*;1)

3
.....wf..... 
1. r : RngSig
⊢ IsRing(|r|;+r;0;-r;*;1) ∈ Type

---

Latex:

---

Latex:

\mBbbZ{}-rng  \mmember{}  Rng


By

---

Latex:
MemTypeCD

---

Home Index