---

Step * 1 1 1 of Lemma free-dma-hom-is-lattice-hom


1. T : Type
2. eq : EqDecider(T)
3. dm : BoundedDistributiveLattice
4. free-DeMorgan-lattice(T;eq) ∈ BoundedLatticeStructure
5. free-DeMorgan-lattice(T;eq) ∈ BoundedLatticeStructure
⊢ free-DeMorgan-lattice(T;eq)["neg" := λx.¬(x)] ∈ BoundedLatticeStructure
BY
{ ((GenConclTerm ⌜free-DeMorgan-lattice(T;eq)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λx.¬(x)) = F ∈ Top⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. v : BoundedLatticeStructure@i'
2. F : Top@i
⊢ v["neg" := F] ∈ BoundedLatticeStructure

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  dm  :  BoundedDistributiveLattice
4.  free-DeMorgan-lattice(T;eq)  \mmember{}  BoundedLatticeStructure
5.  free-DeMorgan-lattice(T;eq)  \mmember{}  BoundedLatticeStructure
\mvdash{}  free-DeMorgan-lattice(T;eq)["neg"  :=  \mlambda{}x.\mneg{}(x)]  \mmember{}  BoundedLatticeStructure


By

---

Latex:
((GenConclTerm  \mkleeneopen{}free-DeMorgan-lattice(T;eq)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}x.\mneg{}(x))  =  F\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index