---

Step * of Lemma face_lattice-basis

∀I:fset(ℕ). ∀x:Point(face_lattice(I)).
  ∃fs:fset({p:fset(names(I)) × fset(names(I))| ↑fset-disjoint(NamesDeq;fst(p);snd(p))} )
   (x = \/(λpr.irr_face(I;fst(pr);snd(pr))"(fs)) ∈ Point(face_lattice(I)))
BY
{ (Intros
   THEN D 0 With ⌜face_lattice_components(I;x)⌝ 
   THEN Auto
   THEN (GenConclTerm ⌜face_lattice_components(I;x)⌝⋅ THENA Auto)
   THEN D -2
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{}).  \mforall{}x:Point(face\_lattice(I)).
    \mexists{}fs:fset(\{p:fset(names(I))  \mtimes{}  fset(names(I))|  \muparrow{}fset-disjoint(NamesDeq;fst(p);snd(p))\}  )
      (x  =  \mbackslash{}/(\mlambda{}pr.irr\_face(I;fst(pr);snd(pr))"(fs)))


By

---

Latex:
(Intros
  THEN  D  0  With  \mkleeneopen{}face\_lattice\_components(I;x)\mkleeneclose{} 
  THEN  Auto
  THEN  (GenConclTerm  \mkleeneopen{}face\_lattice\_components(I;x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Trivial)

---

Home Index