---

Step * of Lemma rv-add-sep1

∀rv:RealVectorSpace. ∀x,x',y:Point.  (x + y # x' + y ⇒ x # x')
BY
{ (InstLemma `rv-add-sep` []
   THEN ParallelLast'
   THEN Auto
   THEN (FHyp 2 [-1] THENM D -1)
   THEN Auto
   THEN (Assert ¬y # y BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:RealVectorSpace.  \mforall{}x,x',y:Point.    (x  +  y  \#  x'  +  y  {}\mRightarrow{}  x  \#  x')


By

---

Latex:
(InstLemma  `rv-add-sep`  []
  THEN  ParallelLast'
  THEN  Auto
  THEN  (FHyp  2  [-1]  THENM  D  -1)
  THEN  Auto
  THEN  (Assert  \mneg{}y  \#  y  BY
                          Auto)
  THEN  Auto)

---

Home Index