---

Step * of Lemma rv-add-sep

∀rv:RealVectorSpace. ∀x,x',y,y':Point.  (x + y # x' + y' ⇒ (x # x' ∨ y # y'))
BY
{ ((D 0 THENA Auto) THEN UseWitness ⌜rv."+sep"⌝⋅ THEN (D 1 THENA Auto) THEN RepUR ``rv-add`` 0 THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}rv."+sep"\mkleeneclose{}\mcdot{}
  THEN  (D  1  THENA  Auto)
  THEN  RepUR  ``rv-add``  0
  THEN  Trivial)

---

Home Index