---

Step * of Lemma lattice-join-0

∀[l:BoundedLattice]. ∀[x:Point(l)].  ((0 ∨ x = x ∈ Point(l)) ∧ (x ∨ 0 = x ∈ Point(l)))
BY
{ (Auto THEN D 1 THEN Auto) }

1
1. l : BoundedLatticeStructure
2. lattice-axioms(l)
3. bounded-lattice-axioms(l)
4. x : Point(l)
⊢ 0 ∨ x = x ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}[l:BoundedLattice].  \mforall{}[x:Point(l)].    ((0  \mvee{}  x  =  x)  \mwedge{}  (x  \mvee{}  0  =  x))


By

---

Latex:
(Auto  THEN  D  1  THEN  Auto)

---

Home Index