---

Step * of Lemma lattice-join-idempotent

∀[l:Lattice]. ∀[u:Point(l)].  (u ∨ u = u ∈ Point(l))
BY
{ ((Auto THEN D 1) 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 ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}[l:Lattice].  \mforall{}[u:Point(l)].    (u  \mvee{}  u  =  u)


By

---

Latex:
((Auto  THEN  D  1)  THEN  Auto)

---

Home Index