---

Step * 1 1 of Lemma lattice-join-idempotent


1. l : LatticeStructure
2. ∀[a,b:Point(l)].  (a ∧ b = b ∧ a ∈ Point(l))
3. ∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l))
4. ∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
5. ∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
6. ∀[a,b:Point(l)].  (a ∨ a ∧ b = a ∈ Point(l))
7. ∀[a,b:Point(l)].  (a ∧ a ∨ b = a ∈ Point(l))
8. u : Point(l)
⊢ u ∨ u ∧ u ∨ u = u ∈ Point(l)
BY
{ (RWO "6" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  l  :  LatticeStructure
2.  \mforall{}[a,b:Point(l)].    (a  \mwedge{}  b  =  b  \mwedge{}  a)
3.  \mforall{}[a,b:Point(l)].    (a  \mvee{}  b  =  b  \mvee{}  a)
4.  \mforall{}[a,b,c:Point(l)].    (a  \mwedge{}  b  \mwedge{}  c  =  a  \mwedge{}  b  \mwedge{}  c)
5.  \mforall{}[a,b,c:Point(l)].    (a  \mvee{}  b  \mvee{}  c  =  a  \mvee{}  b  \mvee{}  c)
6.  \mforall{}[a,b:Point(l)].    (a  \mvee{}  a  \mwedge{}  b  =  a)
7.  \mforall{}[a,b:Point(l)].    (a  \mwedge{}  a  \mvee{}  b  =  a)
8.  u  :  Point(l)
\mvdash{}  u  \mvee{}  u  \mwedge{}  u  \mvee{}  u  =  u


By

---

Latex:
(RWO  "6"  0  THEN  Auto)

---

Home Index