---

Step * of Lemma face-lattice-subset-le

∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).  (x ⊆ y ⇒ x ≤ y)
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (Assert Point(face-lattice(T;eq)) ⊆r fset(fset(T + T)) BY
               (RWO "fl-point-sq" 0 THEN Auto))
   THEN Auto
   THEN BLemma `face-lattice-le`
   THEN Auto) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. x : Point(face-lattice(T;eq))@i
4. y : Point(face-lattice(T;eq))@i
5. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
6. x ⊆ y@i
7. s : fset(T + T)@i
8. s ∈ x@i
⊢ ↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}x,y:Point(face-lattice(T;eq)).    (x  \msubseteq{}  y  {}\mRightarrow{}  x  \mleq{}  y)


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (Assert  Point(face-lattice(T;eq))  \msubseteq{}r  fset(fset(T  +  T))  BY
                          (RWO  "fl-point-sq"  0  THEN  Auto))
  THEN  Auto
  THEN  BLemma  `face-lattice-le`
  THEN  Auto)

---

Home Index