---

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


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)
BY
{ (SubsumeC ⌜Top⌝⋅ THEN Auto THEN BLemma `top-subtype-record`) }

---

Latex:

---

Latex:

1.  L  :  BoundedLatticeStructure
2.  n  :  Top
3.  L  \mmember{}  record(x.Top)
4.  L["neg"  :=  n]  \mmember{}  record(x.Top)
\mvdash{}  L  =  L["neg"  :=  n]


By

---

Latex:
(SubsumeC  \mkleeneopen{}Top\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  BLemma  `top-subtype-record`)

---

Home Index