---

Step * of Lemma ip-triangle-not-between

∀[rv:InnerProductSpace]. ∀[a,b,c:Point].  ¬a_b_c supposing Δ(a;b;c)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN RepUR ``ip-triangle ip-between`` 0
   THEN GenConclTerms Auto [⌜a - b⌝;⌜c - b⌝]⋅
   THEN All Thin
   THEN Auto) }

1
1. rv : InnerProductSpace
2. v : Point
3. v1 : Point
4. |v ⋅ v1| < (||v|| * ||v1||)
⊢ ¬(((||v|| * ||v1||) + v ⋅ v1) = r0)

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b,c:Point].    \mneg{}a\_b\_c  supposing  \mDelta{}(a;b;c)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``ip-triangle  ip-between``  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  -  b\mkleeneclose{};\mkleeneopen{}c  -  b\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto)

---

Home Index