---

Step * of Lemma distributive-lattice-dual-distrib2

∀[L:DistributiveLattice]. ∀[a,b,c:Point(L)].  (b ∧ c ∨ a = b ∨ a ∧ c ∨ a ∈ Point(L))
BY
{ (Auto THEN (Assert L ∈ DistributiveLattice BY Auto) THEN D 1 THEN Auto THEN D 2 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:DistributiveLattice].  \mforall{}[a,b,c:Point(L)].    (b  \mwedge{}  c  \mvee{}  a  =  b  \mvee{}  a  \mwedge{}  c  \mvee{}  a)


By

---

Latex:
(Auto  THEN  (Assert  L  \mmember{}  DistributiveLattice  BY  Auto)  THEN  D  1  THEN  Auto  THEN  D  2  THEN  Auto)

---

Home Index