---

Step * 1 of Lemma trivial-subinterval


1. I : Interval
2. icompact(I)
⊢ [left-endpoint(I), right-endpoint(I)] ⊆ I 
BY
{ (BLemma `rcc-subinterval` THEN EAuto 1) }

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `rcc-subinterval`  THEN  EAuto  1)

---

Home Index