---

Step * of Lemma minus-minus

∀[x:ℤ]. (--x ~ x)
BY
{ ((UnivCD THENA Auto) THEN Assert ⌜(--x) = x ∈ ℤ⌝⋅) }

1
.....assertion..... 
1. x : ℤ
⊢ (--x) = x ∈ ℤ

2
1. x : ℤ
2. (--x) = x ∈ ℤ
⊢ --x ~ x

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (--x  \msim{}  x)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Assert  \mkleeneopen{}(--x)  =  x\mkleeneclose{}\mcdot{})

---

Home Index