---

Step * of Lemma ip-triangle-shift

∀rv:InnerProductSpace. ∀a,b,c:Point.  (Δ(a;b;c) ⇒ (∀z:Point. (z # b ⇒ (¬Δ(a;b;z)) ⇒ Δ(z;b;c))))
BY
{ (Auto THEN FLemma `not-ip-triangle` [-1] THEN Auto THEN ExRepD) }

1
.....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

2
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)
9. t : ℝ
10. r0 < |t|
11. z ≡ b + t*a - b
⊢ Δ(z;b;c)

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point.    (\mDelta{}(a;b;c)  {}\mRightarrow{}  (\mforall{}z:Point.  (z  \#  b  {}\mRightarrow{}  (\mneg{}\mDelta{}(a;b;z))  {}\mRightarrow{}  \mDelta{}(z;b;c))))


By

---

Latex:
(Auto  THEN  FLemma  `not-ip-triangle`  [-1]  THEN  Auto  THEN  ExRepD)

---

Home Index