---

Step * 2 2 2 of Lemma mk-DeMorgan-algebra_wf


1. L : BoundedDistributiveLattice
2. n : Point(L) ⟶ Point(L)
3. ∀x:Point(L). ((n (n x)) = x ∈ Point(L))
4. (∀x,y:Point(L).  ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n y ∈ Point(L)))
5. L["neg" := n] ∈ BoundedLatticeStructure
6. L["neg" := n] ∈ DeMorganAlgebraStructure
7. L["neg" := n] = L ∈ BoundedDistributiveLattice
⊢ mk-DeMorgan-algebra(L;n) ∈ DeMorganAlgebra
BY
{ ((Assert L ∈ BoundedDistributiveLattice BY
          Auto)
   THEN D 1
   THEN Unfold `mk-DeMorgan-algebra` 0
   THEN MemTypeCD
   THEN Auto) }

1
1. L : BoundedLatticeStructure
2. lattice-axioms(L)
3. bounded-lattice-axioms(L)
4. ∀[a,b,c:Point(L)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(L))
5. n : Point(L) ⟶ Point(L)
6. ∀x:Point(L). ((n (n x)) = x ∈ Point(L))
7. (∀x,y:Point(L).  ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n y ∈ Point(L)))
8. L["neg" := n] ∈ BoundedLatticeStructure
9. L["neg" := n] ∈ DeMorganAlgebraStructure
10. L["neg" := n] = L ∈ BoundedDistributiveLattice
11. L ∈ BoundedDistributiveLattice
12. lattice-axioms(L["neg" := n])
13. bounded-lattice-axioms(L["neg" := n])
14. ∀[a,b,c:Point(L["neg" := n])].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(L["neg" := n]))
⊢ DeMorgan-algebra-axioms(L["neg" := n])

---

Latex:

---

Latex:

1.  L  :  BoundedDistributiveLattice
2.  n  :  Point(L)  {}\mrightarrow{}  Point(L)
3.  \mforall{}x:Point(L).  ((n  (n  x))  =  x)
4.  (\mforall{}x,y:Point(L).    ((n  x  \mwedge{}  y)  =  n  x  \mvee{}  n  y))  \mvee{}  (\mforall{}x,y:Point(L).    ((n  x  \mvee{}  y)  =  n  x  \mwedge{}  n  y))
5.  L["neg"  :=  n]  \mmember{}  BoundedLatticeStructure
6.  L["neg"  :=  n]  \mmember{}  DeMorganAlgebraStructure
7.  L["neg"  :=  n]  =  L
\mvdash{}  mk-DeMorgan-algebra(L;n)  \mmember{}  DeMorganAlgebra


By

---

Latex:
((Assert  L  \mmember{}  BoundedDistributiveLattice  BY
                Auto)
  THEN  D  1
  THEN  Unfold  `mk-DeMorgan-algebra`  0
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index