---

Step * of Lemma fl1-not-1

∀[I:fset(ℕ)]. ∀[x:names(I)].  (¬((x=1) = 1 ∈ Point(face_lattice(I))))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RepUR ``fl1 face-lattice1 lattice-1 face_lattice face-lattice`` -1
   THEN RepUR ``lattice-point free-dist-lattice-with-constraints`` -1
   THEN RepUR ``constrained-antichain-lattice mk-bounded-distributive-lattice`` -1
   THEN RepUR ``mk-bounded-lattice`` -1
   THEN (EqTypeHD (-1) THENA Auto)
   THEN Thin (-1)) }

1
1. I : fset(ℕ)
2. x : names(I)
3. {{inr x }} = {{}} ∈ fset(fset(names(I) + names(I)))
⊢ False

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (\mneg{}((x=1)  =  1))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``fl1  face-lattice1  lattice-1  face\_lattice  face-lattice``  -1
  THEN  RepUR  ``lattice-point  free-dist-lattice-with-constraints``  -1
  THEN  RepUR  ``constrained-antichain-lattice  mk-bounded-distributive-lattice``  -1
  THEN  RepUR  ``mk-bounded-lattice``  -1
  THEN  (EqTypeHD  (-1)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index