---

Step * 1 of Lemma mk-DeMorgan-algebra-equal-bounded-lattice


1. L : BoundedLatticeStructure
2. n : Top
⊢ L["neg" := n] = L ∈ BoundedLatticeStructure
BY
{ (Auto
   THEN Symmetry
   THEN (RecordExt THEN Try (Trivial))
   THEN Try ((Reduce 0
              THEN Folds ``lattice-point lattice-0 lattice-1`` 0
              THEN ((RepeatFor 2 ((FunExt THENA Auto)) THEN Folds ``lattice-meet lattice-join`` 0 THEN Auto)
              ORELSE Auto
              )))) }

1
.....wf..... 
1. L : BoundedLatticeStructure
2. n : Top
3. L ∈ BoundedLatticeStructure
⊢ L["neg" := n] ∈ BoundedLatticeStructure

2
1. L : BoundedLatticeStructure
2. n : Top
3. L ∈ record(x.Top)
4. L["neg" := n] ∈ record(x.Top)
⊢ L = L["neg" := n] ∈ record(x.Top)

---

Latex:

---

Latex:

1.  L  :  BoundedLatticeStructure
2.  n  :  Top
\mvdash{}  L["neg"  :=  n]  =  L


By

---

Latex:
(Auto
  THEN  Symmetry
  THEN  (RecordExt  THEN  Try  (Trivial))
  THEN  Try  ((Reduce  0
                        THEN  Folds  ``lattice-point  lattice-0  lattice-1``  0
                        THEN  ((RepeatFor  2  ((FunExt  THENA  Auto))
                                      THEN  Folds  ``lattice-meet  lattice-join``  0
                                      THEN  Auto)
                        ORELSE  Auto
                        ))))

---

Home Index