---

Step * 1 of Lemma nc-se'-p


1. J : fset(ℕ)
2. k : ℕ
3. z : ℕ
4. n : {n:ℕ| ¬n ∈ J} 
5. x : names(J+z)
6. x = z ∈ ℤ
⊢ ((n/<k>) n) = <k> ∈ Point(dM(J+k))
BY
{ (RepUR ``nc-p`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  J  :  fset(\mBbbN{})
2.  k  :  \mBbbN{}
3.  z  :  \mBbbN{}
4.  n  :  \{n:\mBbbN{}|  \mneg{}n  \mmember{}  J\} 
5.  x  :  names(J+z)
6.  x  =  z
\mvdash{}  ((n/<k>)  n)  =  <k>


By

---

Latex:
(RepUR  ``nc-p``  0  THEN  AutoSplit)

---

Home Index