---

Step * of Lemma subinterval-trivial

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

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

---

Latex:

---

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


By

---

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

---

Home Index