---

Step * of Lemma fills-open_box_wf

∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
  ∀[bx:open_box(X;I;J;x;i)]. ∀[cube:X(I)].  (fills-open_box(X;I;bx;cube) ∈ ℙ) supposing l_subset(Cname;J;I)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,J:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
    \mforall{}[bx:open\_box(X;I;J;x;i)].  \mforall{}[cube:X(I)].    (fills-open\_box(X;I;bx;cube)  \mmember{}  \mBbbP{}) 
    supposing  l\_subset(Cname;J;I)


By

---

Latex:
ProveWfLemma

---

Home Index