---

Step * 1 1 of Lemma iproper-subinterval


1. J : Interval
2. a : ℝ
3. b : ℝ
⊢ [a, b] ⊆ J  ⇒ iproper([a, b]) ⇒ iproper(J)
BY
{ (Auto THEN RepUR ``iproper i-finite`` -1 THEN (D -1 THENA Auto)) }

1
1. J : Interval
2. a : ℝ
3. b : ℝ
4. [a, b] ⊆ J 
5. a < b
⊢ iproper(J)

---

Latex:

---

Latex:

1.  J  :  Interval
2.  a  :  \mBbbR{}
3.  b  :  \mBbbR{}
\mvdash{}  [a,  b]  \msubseteq{}  J    {}\mRightarrow{}  iproper([a,  b])  {}\mRightarrow{}  iproper(J)


By

---

Latex:
(Auto  THEN  RepUR  ``iproper  i-finite``  -1  THEN  (D  -1  THENA  Auto))

---

Home Index