---

Step * 1 of Lemma subinterval-trivial


1. I : Interval
2. icompact(I)
⊢ I ⊆ [left-endpoint(I), right-endpoint(I)] 
BY
{ ((D 0 THEN Auto)
   THEN D 1
   THEN DProdsAndUnions
   THEN (All (RepUR ``left-endpoint right-endpoint endpoints icompact``)
         THEN All (RepUR ``i-closed i-finite i-member``)
         )
   THEN ExRepD
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
\mvdash{}  I  \msubseteq{}  [left-endpoint(I),  right-endpoint(I)] 


By

---

Latex:
((D  0  THEN  Auto)
  THEN  D  1
  THEN  DProdsAndUnions
  THEN  (All  (RepUR  ``left-endpoint  right-endpoint  endpoints  icompact``)
              THEN  All  (RepUR  ``i-closed  i-finite  i-member``)
              )
  THEN  ExRepD
  THEN  Auto)

---

Home Index