proposition: Lemma Continuous_I_imp_tb_image : totally_bounded (fun_image F I).
proof: Proof. cut (Continuous_I (Lend_leEq_Rend _ cI) F). intro H. elim (Continuous_I_imp_tb_image _ _ _ _ H); intros. split; [ clear b | clear a ]. elim a; intros x Hx. elim Hx; intros y Hy. elim Hy; clear a Hx Hy; intros Hy Hx. elim Hx; clear Hx; intros Hy'' Hx. exists x; exists y. split. exact (compact_interval_inc _ _ _ _ Hy). auto. intros e He. elim (b e He); intros l H0 H1. exists l; clear b; [ clear H1 | clear H0 ]. intros x Hx. elim (H0 x Hx); intros y Hy. elim Hy; clear H0 Hy Hx; intros Hy Hx. elim Hx; clear Hx; intros Hy' Hx. exists y. split. exact (compact_interval_inc _ _ _ _ Hy). auto. intros x H0. apply H1. clear H1. elim H0; intros y Hy. elim Hy; clear H0 Hy; intros Hy Hx. elim Hx; clear Hx; intros Hy' Hx. exists y. split. exact (interval_compact_inc _ _ (Lend_leEq_Rend _ cI) _ Hy). auto. apply continuous_compact. Qed.
imports: CoRN.ftc.MoreIntervals