---

Step * of Lemma distributive-lattice-distrib

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

1
1. L : LatticeStructure
2. lattice-axioms(L)
3. ∀[a,b,c:Point(L)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(L))
4. a : Point(L)
5. b : Point(L)
6. c : Point(L)
7. a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(L)
⊢ b ∨ c ∧ a = b ∧ a ∨ c ∧ a ∈ Point(L)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  1  THEN  Auto)

---

Home Index