---

Step * of Lemma face-lattice-0-not-1

∀[J:fset(ℕ)]. (¬(0 = 1 ∈ Point(face_lattice(J))))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. J : fset(ℕ)
2. 0 = 1 ∈ Point(face_lattice(J))
⊢ False

---

Latex:

---

Latex:
\mforall{}[J:fset(\mBbbN{})].  (\mneg{}(0  =  1))


By

---

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

---

Home Index