proposition: Lemma Included_imp_Continuous : forall J : interval, included J I -> Continuous J F.
proof: Proof. intros J H. split. exact (included_trans _ _ _ _ H (Continuous_imp_inc _ _ contF)). intros. apply included_imp_Continuous; Included. Qed.
imports: CoRN.ftc.MoreIntervals