---

Step * 1 of Lemma ip-congruent-same2


1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. ||a - b|| = r0
6. c - c ≡ 0
⊢ a ≡ b
BY
{ (RWO "rv-norm-is-zero" (-2) THEN EAuto 1) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  ||a  -  b||  =  r0
6.  c  -  c  \mequiv{}  0
\mvdash{}  a  \mequiv{}  b


By

---

Latex:
(RWO  "rv-norm-is-zero"  (-2)  THEN  EAuto  1)

---

Home Index