---

Step * of Lemma DeMorgan-algebra-laws

∀[dma:DeMorganAlgebra]
  ((∀x:Point(dma). (¬(¬(x)) = x ∈ Point(dma)))
  ∧ (∀x,y:Point(dma).  (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dma)))
  ∧ (∀x,y:Point(dma).  (¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dma)))
  ∧ (¬(0) = 1 ∈ Point(dma))
  ∧ (¬(1) = 0 ∈ Point(dma)))
BY
{ ((D 0 THENA Auto) THEN (Assert dma ∈ DeMorganAlgebra BY Auto) THEN D 1 THEN Auto) }

1
1. dma : DeMorganAlgebraStructure
2. lattice-axioms(dma)
3. bounded-lattice-axioms(dma)
4. ∀[a,b,c:Point(dma)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(dma))
5. DeMorgan-algebra-axioms(dma)
6. dma ∈ DeMorganAlgebra
7. ∀x:Point(dma). (¬(¬(x)) = x ∈ Point(dma))
8. ∀x,y:Point(dma).  (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dma))
9. x : Point(dma)
10. y : Point(dma)
⊢ ¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dma)

2
1. dma : DeMorganAlgebraStructure
2. lattice-axioms(dma)
3. bounded-lattice-axioms(dma)
4. ∀[a,b,c:Point(dma)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(dma))
5. DeMorgan-algebra-axioms(dma)
6. dma ∈ DeMorganAlgebra
7. ∀x:Point(dma). (¬(¬(x)) = x ∈ Point(dma))
8. ∀x,y:Point(dma).  (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dma))
9. ∀x,y:Point(dma).  (¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dma))
⊢ ¬(0) = 1 ∈ Point(dma)

---

Latex:

---

Latex:
\mforall{}[dma:DeMorganAlgebra]
    ((\mforall{}x:Point(dma).  (\mneg{}(\mneg{}(x))  =  x))
    \mwedge{}  (\mforall{}x,y:Point(dma).    (\mneg{}(x  \mwedge{}  y)  =  \mneg{}(x)  \mvee{}  \mneg{}(y)))
    \mwedge{}  (\mforall{}x,y:Point(dma).    (\mneg{}(x  \mvee{}  y)  =  \mneg{}(x)  \mwedge{}  \mneg{}(y)))
    \mwedge{}  (\mneg{}(0)  =  1)
    \mwedge{}  (\mneg{}(1)  =  0))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (Assert  dma  \mmember{}  DeMorganAlgebra  BY  Auto)  THEN  D  1  THEN  Auto)

---

Home Index