---

Step * 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 ∈ Point(l)
BY
{ (Subst' u ∨ u = u ∨ u ∧ u ∨ u ∈ Point(l) 0 THENA (Try ((EqCD THEN Auto)) THEN Auto)) }

1
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)

---

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  =  u


By

---

Latex:
(Subst'  u  \mvee{}  u  =  u  \mvee{}  u  \mwedge{}  u  \mvee{}  u  0  THENA  (Try  ((EqCD  THEN  Auto))  THEN  Auto))

---

Home Index