---

Step * of Lemma assert-fl-eq

∀[I:fset(ℕ)]. ∀[x,y:Point(face_lattice(I))].  uiff(↑(x==y);x = y ∈ Point(face_lattice(I)))
BY
{ ((UnivCD THENA Auto)
   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)
         )
   ) }

1
1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
4. Point(face_lattice(I)) ⊆r Point(free-DeMorgan-lattice(names(I);NamesDeq))
⊢ uiff(↑(x==y);x = y ∈ Point(face_lattice(I)))

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  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)
              )
  )

---

Home Index