---

Step * 2 2 1 1 2 of Lemma fl-meet-0-1


1. T : Type
2. eq : EqDecider(T)
3. ee : EqDecider(Point(face-lattice(T;eq)))
4. deq-fset(deq-fset(union-deq(T;T;eq;eq))) = ee ∈ EqDecider(Point(face-lattice(T;eq)))
⊢ ∀a,b:Point(face-lattice(T;eq)).
    ((/\({} ⋃ {a} ⋃ {b}) = 0 ∈ Point(face-lattice(T;eq))) ⇒ (a ∧ b = 0 ∈ Point(face-lattice(T;eq))))
BY
{ (Thin (-1) THEN MoveToConcl (-1) THEN (GenConclTerm ⌜face-lattice(T;eq)⌝⋅ THENA Auto) THEN All Thin THEN Auto) }

1
1. v : BoundedDistributiveLattice
2. ee : EqDecider(Point(v))
3. a : Point(v)
4. b : Point(v)
5. /\({} ⋃ {a} ⋃ {b}) = 0 ∈ Point(v)
⊢ a ∧ b = 0 ∈ Point(v)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  ee  :  EqDecider(Point(face-lattice(T;eq)))
4.  deq-fset(deq-fset(union-deq(T;T;eq;eq)))  =  ee
\mvdash{}  \mforall{}a,b:Point(face-lattice(T;eq)).    ((/\mbackslash{}(\{\}  \mcup{}  \{a\}  \mcup{}  \{b\})  =  0)  {}\mRightarrow{}  (a  \mwedge{}  b  =  0))


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}face-lattice(T;eq)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index