---

Step * of Lemma sq_stable__integ_dom_p

∀[r:CRng]. SqStable(IsIntegDom(r))
BY
{ Unfold `integ_dom_p` 0  
THEN UnivCD THENA Auto }

1
1. r : CRng
⊢ SqStable(0 ≠ 1 ∈ |r|  ∧ (∀u,v:|r|.  ((¬(v = 0 ∈ |r|)) ⇒ ((u * v) = 0 ∈ |r|) ⇒ (u = 0 ∈ |r|))))

---

Latex:

---

Latex:
\mforall{}[r:CRng].  SqStable(IsIntegDom(r))


By

---

Latex:
Unfold  `integ\_dom\_p`  0   
THEN  UnivCD  THENA  Auto

---

Home Index