---

Step * 1 of Lemma ip-triangle-shift

.....antecedent..... 
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. Δ(a;b;c)
6. z : Point
7. z # b
8. ¬Δ(a;b;z)
⊢ a # b
BY
{ (FLemma `ip-triangle-implies-separated2` [-4] THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  \mDelta{}(a;b;c)
6.  z  :  Point
7.  z  \#  b
8.  \mneg{}\mDelta{}(a;b;z)
\mvdash{}  a  \#  b


By

---

Latex:
(FLemma  `ip-triangle-implies-separated2`  [-4]  THEN  Auto)

---

Home Index