---

Step * of Lemma member-empty-cubical-subset

∀[I:fset(ℕ)]. ∀[phi:Point(face_lattice(I))].
  ∀[X,A:Top].  (A ∈ {I,phi ⊢ _:X}) supposing phi = 0 ∈ Point(face_lattice(I))
BY
{ (InstLemma `empty-cubical-subset-term` [] THEN RepeatFor 5 (ParallelLast')) }

1
1. I : fset(ℕ)
2. phi : Point(face_lattice(I))
3. phi = 0 ∈ Point(face_lattice(I))
4. [X] : Top
5. [A] : Top
6. ∀[B:Top]. (A = B ∈ {I,phi ⊢ _:X})
⊢ A ∈ {I,phi ⊢ _:X}

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:Point(face\_lattice(I))].    \mforall{}[X,A:Top].    (A  \mmember{}  \{I,phi  \mvdash{}  \_:X\})  supposing  phi  =  0


By

---

Latex:
(InstLemma  `empty-cubical-subset-term`  []  THEN  RepeatFor  5  (ParallelLast'))

---

Home Index