---

Step * of Lemma isdM1_wf

∀[I:fset(ℕ)]. ∀[x:Point(dM(I))].  (isdM1(x) ∈ 𝔹)
BY
{ ((Auto THEN (RWO "dM-point" (-1) THENA Auto)) THEN D -1 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:Point(dM(I))].    (isdM1(x)  \mmember{}  \mBbbB{})


By

---

Latex:
((Auto  THEN  (RWO  "dM-point"  (-1)  THENA  Auto))  THEN  D  -1  THEN  ProveWfLemma)

---

Home Index