---

Step * of Lemma nc-1-lemma

No Annotations
∀J:fset(ℕ). ∀j:ℕ. ∀i:{i:names(J)| ¬i ∈ J} .  (((j1) i) = <i> ∈ Point(dM(J)))
BY
{ ((Auto THEN RepUR ``nc-1`` 0) THEN AutoSplit) }

1
1. J : fset(ℕ)
2. j : ℕ
3. i : {i:names(J)| ¬i ∈ J} 
4. i = j ∈ ℤ
⊢ {{}} = <i> ∈ Point(dM(J))

---

Latex:

---

Latex:
No  Annotations
\mforall{}J:fset(\mBbbN{}).  \mforall{}j:\mBbbN{}.  \mforall{}i:\{i:names(J)|  \mneg{}i  \mmember{}  J\}  .    (((j1)  i)  =  <i>)


By

---

Latex:
((Auto  THEN  RepUR  ``nc-1``  0)  THEN  AutoSplit)

---

Home Index