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. 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