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