---

Step * of Lemma ring_triv

∀[r:Rng]. ∀[a:|r|]. (a = 0 ∈ |r|) supposing 1 = 0 ∈ |r|
BY
{ ((RepD) THENA Auto) }

1
1. r : Rng
2. 1 = 0 ∈ |r|
3. a : |r|
⊢ a = 0 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a:|r|].  (a  =  0)  supposing  1  =  0


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index