---

Step * of Lemma dma-neg-eq-1-implies-meet-eq-0

∀[K:fset(ℕ)]. ∀[a2,x1:Point(dM(K))].  ((¬(a2) = 1 ∈ Point(dM(K))) ⇒ (0 = a2 ∧ x1 ∈ Point(dM(K))))
BY
{ (Auto
   THEN (InstLemma `dM-neg-properties` [⌜K⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert ⌜0 = ¬(¬(a2 ∧ x1)) ∈ Point(dM(K))⌝⋅ THENM (RWO "-2" (-1) THEN Auto))) }

1
.....assertion..... 
1. K : fset(ℕ)
2. a2 : Point(dM(K))
3. x1 : Point(dM(K))
4. ¬(a2) = 1 ∈ Point(dM(K))
5. ∀[x,y:Point(dM(K))].  (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dM(K)))
6. ∀[x,y:Point(dM(K))].  (¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dM(K)))
7. ∀[x:Point(dM(K))]. (¬(¬(x)) = x ∈ Point(dM(K)))
⊢ 0 = ¬(¬(a2 ∧ x1)) ∈ Point(dM(K))

---

Latex:

---

Latex:
\mforall{}[K:fset(\mBbbN{})].  \mforall{}[a2,x1:Point(dM(K))].    ((\mneg{}(a2)  =  1)  {}\mRightarrow{}  (0  =  a2  \mwedge{}  x1))


By

---

Latex:
(Auto
  THEN  (InstLemma  `dM-neg-properties`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}0  =  \mneg{}(\mneg{}(a2  \mwedge{}  x1))\mkleeneclose{}\mcdot{}  THENM  (RWO  "-2"  (-1)  THEN  Auto)))

---

Home Index