---

Step * 1 of Lemma rv-add_functionality


1. rv : RealVectorSpace
2. x : Point
3. y : Point
4. x' : Point
5. y' : Point
6. x ≡ x'
7. y ≡ y'
8. x + y # x' + y'
9. x' + y' # x' + y
10. y' # y
⊢ False
BY
{ (D -4 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  rv  :  RealVectorSpace
2.  x  :  Point
3.  y  :  Point
4.  x'  :  Point
5.  y'  :  Point
6.  x  \mequiv{}  x'
7.  y  \mequiv{}  y'
8.  x  +  y  \#  x'  +  y'
9.  x'  +  y'  \#  x'  +  y
10.  y'  \#  y
\mvdash{}  False


By

---

Latex:
(D  -4  THEN  EAuto  1)

---

Home Index