---

Step * of Lemma ip-triangle-implies

∀rv:InnerProductSpace. ∀a,b,c:Point.
  (Δ(a;b;c) ⇒ (Δ(c;b;a) ∧ Δ(c;a;b) ∧ a # c ∧ (¬a_b_c) ∧ (∀z:Point. (z # b ⇒ (¬Δ(a;b;z)) ⇒ Δ(z;b;c)))))
BY
{ (EAuto 1
   THEN Try ((FLemma `ip-triangle-implies-separated` [-3] THEN Auto))
   THEN InstLemma `ip-triangle-shift` [⌜rv⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜z⌝]⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(EAuto  1
  THEN  Try  ((FLemma  `ip-triangle-implies-separated`  [-3]  THEN  Auto))
  THEN  InstLemma  `ip-triangle-shift`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index