---

Step * of Lemma ip-triangle-implies-separated2

∀rv:InnerProductSpace. ∀a,b,c:Point.  (Δ(a;b;c) ⇒ a # b)
BY
{ (Auto
   THEN RepeatFor 2 ((FLemma `ip-triangle-permute` [-1] THENA Auto))
   THEN FLemma `ip-triangle-implies-separated` [-1]
   THEN Auto) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. Δ(a;b;c)
6. Δ(c;a;b)
7. Δ(b;c;a)
8. b # a
⊢ a # b

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((FLemma  `ip-triangle-permute`  [-1]  THENA  Auto))
  THEN  FLemma  `ip-triangle-implies-separated`  [-1]
  THEN  Auto)

---

Home Index