Step * of Lemma i-finite-subinterval

I,J:Interval.  (I ⊆ J   i-finite(J)  i-finite(I))
BY
(RWO "i-finite-iff-bounded" THEN Auto) }


Latex:


Latex:
\mforall{}I,J:Interval.    (I  \msubseteq{}  J    {}\mRightarrow{}  i-finite(J)  {}\mRightarrow{}  i-finite(I))


By


Latex:
(RWO  "i-finite-iff-bounded"  0  THEN  Auto)




Home Index