---

Step * 2 2 2 of Lemma dm-neg-is-hom-opposite


1. T : Type
2. eq : EqDecider(T)
⊢ (¬(1) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))) ∧ (¬(0) = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  (\mneg{}(1)  =  0)  \mwedge{}  (\mneg{}(0)  =  1)


By

---

Latex:
Auto

---

Home Index