---

Step * of Lemma lattice_properties

∀[l:Lattice]
  ((∀[a,b:Point(l)].  (a ∧ b = b ∧ a ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l)))
  ∧ (∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l)))
  ∧ (∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∨ a ∧ b = a ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∧ a ∨ b = a ∈ Point(l))))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN (Unhide THENA Auto) THEN D -1 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  (Unhide  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index