---

Step * of Lemma trivial-subinterval

∀I:Interval. [left-endpoint(I), right-endpoint(I)] ⊆ I  supposing icompact(I)
BY
{ (Auto THEN (Assert icompact(I) BY (Unhide THEN Auto)) THEN Thin 2) }

1
1. I : Interval
2. icompact(I)
⊢ [left-endpoint(I), right-endpoint(I)] ⊆ I 

---

Latex:

---

Latex:
\mforall{}I:Interval.  [left-endpoint(I),  right-endpoint(I)]  \msubseteq{}  I    supposing  icompact(I)


By

---

Latex:
(Auto  THEN  (Assert  icompact(I)  BY  (Unhide  THEN  Auto))  THEN  Thin  2)

---

Home Index