---

Step * of Lemma iproper-length-iff

∀I:Interval. (i-finite(I) ⇒ (r0 < |I| ⇐⇒ iproper(I)))
BY
{ Auto }

1
1. I : Interval
2. i-finite(I)
3. r0 < |I|
⊢ iproper(I)

2
1. I : Interval
2. i-finite(I)
3. iproper(I)
⊢ r0 < |I|

---

Latex:

---

Latex:
\mforall{}I:Interval.  (i-finite(I)  {}\mRightarrow{}  (r0  <  |I|  \mLeftarrow{}{}\mRightarrow{}  iproper(I)))


By

---

Latex:
Auto

---

Home Index