---

Step * 2 1 of Lemma mk-DeMorgan-algebra_wf

.....assertion..... 
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
⊢ L["neg" := n] ∈ DeMorganAlgebraStructure
BY
{ (Unfold `DeMorgan-algebra-structure` 0
   THEN Fold `bounded-lattice-structure` 0
   THEN Fold `lattice-point` 0
   THEN D 1
   THEN RecordPlusTypeCD
   THEN Reduce 0
   THEN Try (Trivial)
   THEN RepUR ``lattice-point`` 0
   THEN Fold `lattice-point` 0
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  L["neg"  :=  n]  \mmember{}  DeMorganAlgebraStructure


By

---

Latex:
(Unfold  `DeMorgan-algebra-structure`  0
  THEN  Fold  `bounded-lattice-structure`  0
  THEN  Fold  `lattice-point`  0
  THEN  D  1
  THEN  RecordPlusTypeCD
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  RepUR  ``lattice-point``  0
  THEN  Fold  `lattice-point`  0
  THEN  Auto)

---

Home Index