---

Step * of Lemma iproper-subinterval

No Annotations
∀I,J:Interval.  (I ⊆ J  ⇒ iproper(I) ⇒ iproper(J))
BY
{ Assert ⌜∀I,J:Interval.  (icompact(I) ⇒ I ⊆ J  ⇒ iproper(I) ⇒ iproper(J))⌝⋅ }

1
.....assertion..... 
∀I,J:Interval.  (icompact(I) ⇒ I ⊆ J  ⇒ iproper(I) ⇒ iproper(J))

2
1. ∀I,J:Interval.  (icompact(I) ⇒ I ⊆ J  ⇒ iproper(I) ⇒ iproper(J))
⊢ ∀I,J:Interval.  (I ⊆ J  ⇒ iproper(I) ⇒ iproper(J))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I,J:Interval.    (I  \msubseteq{}  J    {}\mRightarrow{}  iproper(I)  {}\mRightarrow{}  iproper(J))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}I,J:Interval.    (icompact(I)  {}\mRightarrow{}  I  \msubseteq{}  J    {}\mRightarrow{}  iproper(I)  {}\mRightarrow{}  iproper(J))\mkleeneclose{}\mcdot{}

---

Home Index