---

Step * of Lemma neg-dM_opp

∀[I:fset(ℕ)]. ∀[x:names(I)].  (¬(<1-x>) = <x> ∈ Point(dM(I)))
BY
{ (Auto THEN RepUR ``dM_inc dM_opp`` 0 THEN (Unfold `dM` 0 THEN RWO "free-dma-point" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (\mneg{}(ə-x>)  =  <x>)


By

---

Latex:
(Auto  THEN  RepUR  ``dM\_inc  dM\_opp``  0  THEN  (Unfold  `dM`  0  THEN  RWO  "free-dma-point"  0)  THEN  Auto)

---

Home Index