---

Step * of Lemma rv-minus_functionality

∀[rv:RealVectorSpace]. ∀[x,x':Point].  -x ≡ -x' supposing x ≡ x'
BY
{ (Unfold `rv-minus` 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[x,x':Point].    -x  \mequiv{}  -x'  supposing  x  \mequiv{}  x'


By

---

Latex:
(Unfold  `rv-minus`  0  THEN  EAuto  1)

---

Home Index