---

Step * of Lemma fl-eq_wf

∀[I:fset(ℕ)]. ∀[x,y:Point(face_lattice(I))].  ((x==y) ∈ 𝔹)
BY
{ Auto }

1
1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
⊢ (x==y) ∈ 𝔹

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x,y:Point(face\_lattice(I))].    ((x==y)  \mmember{}  \mBbbB{})


By

---

Latex:
Auto

---

Home Index