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