---

Step * of Lemma mk-lattice_wf

∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T].
  mk-lattice(T;m;j) ∈ Lattice 
  supposing (∀[a,b:T].  (m[a;b] = m[b;a] ∈ T))
  ∧ (∀[a,b:T].  (j[a;b] = j[b;a] ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T))
  ∧ (∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T))
  ∧ (∀[a,b:T].  (j[a;m[a;b]] = a ∈ T))
  ∧ (∀[a,b:T].  (m[a;j[a;b]] = a ∈ T))
BY
{ (Auto THEN RepUR ``mk-lattice lattice`` 0) }

1
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. ∀[a,b:T].  (m[a;b] = m[b;a] ∈ T)
5. ∀[a,b:T].  (j[a;b] = j[b;a] ∈ T)
6. ∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T)
7. ∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T)
8. ∀[a,b:T].  (j[a;m[a;b]] = a ∈ T)
9. ∀[a,b:T].  (m[a;j[a;b]] = a ∈ T)
⊢ λx.x["Point" := T]["meet" := m]["join" := j] ∈ {l:LatticeStructure| lattice-axioms(l)} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m,j:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].
    mk-lattice(T;m;j)  \mmember{}  Lattice 
    supposing  (\mforall{}[a,b:T].    (m[a;b]  =  m[b;a]))
    \mwedge{}  (\mforall{}[a,b:T].    (j[a;b]  =  j[b;a]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (m[a;m[b;c]]  =  m[m[a;b];c]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (j[a;j[b;c]]  =  j[j[a;b];c]))
    \mwedge{}  (\mforall{}[a,b:T].    (j[a;m[a;b]]  =  a))
    \mwedge{}  (\mforall{}[a,b:T].    (m[a;j[a;b]]  =  a))


By

---

Latex:
(Auto  THEN  RepUR  ``mk-lattice  lattice``  0)

---

Home Index