---

Step * of Lemma rn-ip-between

No Annotations
∀n:{2...}. ∀a,b,c:ℝ^n.  (a_b_c ⇐⇒ rv-T(n;a;b;c))
BY
{ (Intro THEN (Assert ⌜Point(ipℝ^n) = ℝ^n ∈ Type⌝⋅ THENA (Computation THEN Auto)) THEN RepeatFor 3 (Intro)) }

1
1. n : {2...}
2. Point(ipℝ^n) = ℝ^n ∈ Type
3. a : ℝ^n
4. b : ℝ^n
5. c : ℝ^n
⊢ a_b_c ⇐⇒ rv-T(n;a;b;c)

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\{2...\}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (a\_b\_c  \mLeftarrow{}{}\mRightarrow{}  rv-T(n;a;b;c))


By

---

Latex:
(Intro  THEN  (Assert  \mkleeneopen{}Point(ip\mBbbR{}\^{}n)  =  \mBbbR{}\^{}n\mkleeneclose{}\mcdot{}  THENA  (Computation  THEN  Auto))  THEN  RepeatFor  3  (Intro))

---

Home Index