---

Step * 1 of Lemma dM-lift-s

.....wf..... 
1. I : fset(ℕ)
2. J : fset(ℕ)
3. I ⊆ J
4. x : Point(dM(I))
⊢ I ∈ {J:fset(ℕ)| I ⊆ J} 
BY
{ (MemTypeCD THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  I  \msubseteq{}  J
4.  x  :  Point(dM(I))
\mvdash{}  I  \mmember{}  \{J:fset(\mBbbN{})|  I  \msubseteq{}  J\} 


By

---

Latex:
(MemTypeCD  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index