---

Step * of Lemma rv-sep-shift

∀rv:InnerProductSpace. ∀a,p,q:Point.  (p # q ⇒ p - a # q - a)
BY
{ Auto }

1
1. rv : InnerProductSpace
2. a : Point
3. p : Point
4. q : Point
5. p # q
⊢ p - a # q - a

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,p,q:Point.    (p  \#  q  {}\mRightarrow{}  p  -  a  \#  q  -  a)


By

---

Latex:
Auto

---

Home Index