---

Step * 1 1 1 1 1 1 of Lemma lattice-meet-fset-join-distrib


1. l : BoundedDistributiveLattice
2. eq : EqDecider(Point(l))
3. ∀[a,b,c:Point(l)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l))
4. bs : Point(l) List
⊢ 0 ∧ \/(bs) = 0 ∈ Point(l)
BY
{ Auto }

---

Latex:

---

Latex:

1.  l  :  BoundedDistributiveLattice
2.  eq  :  EqDecider(Point(l))
3.  \mforall{}[a,b,c:Point(l)].    (a  \mwedge{}  b  \mvee{}  c  =  a  \mwedge{}  b  \mvee{}  a  \mwedge{}  c)
4.  bs  :  Point(l)  List
\mvdash{}  0  \mwedge{}  \mbackslash{}/(bs)  =  0


By

---

Latex:
Auto

---

Home Index