---

Step * 1 of Lemma fl-eq_wf


1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
⊢ (x==y) ∈ 𝔹
BY
{ ((Unfold `fl-eq` 0 THEN (GenConclTerm ⌜free-dml-deq(names(I);NamesDeq)⌝⋅ THENA Auto))
   THEN Thin (-1)
   THEN (Assert ⌜Point(face_lattice(I)) ⊆r Point(free-DeMorgan-lattice(names(I);NamesDeq))⌝⋅
         THENA (Unfolds ``face_lattice free-DeMorgan-lattice`` 0 THEN RWO "fl-point free-dl-point" 0 THEN Auto)
         )
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(face\_lattice(I))
3.  y  :  Point(face\_lattice(I))
\mvdash{}  (x==y)  \mmember{}  \mBbbB{}


By

---

Latex:
((Unfold  `fl-eq`  0  THEN  (GenConclTerm  \mkleeneopen{}free-dml-deq(names(I);NamesDeq)\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  Thin  (-1)
  THEN  (Assert  \mkleeneopen{}Point(face\_lattice(I))  \msubseteq{}r  Point(free-DeMorgan-lattice(names(I);NamesDeq))\mkleeneclose{}\mcdot{}
              THENA  (Unfolds  ``face\_lattice  free-DeMorgan-lattice``  0
                            THEN  RWO  "fl-point  free-dl-point"  0
                            THEN  Auto)
              )
  THEN  Auto)

---

Home Index