proposition: Lemma Continuous_wd : Feq I F G -> Continuous I F -> Continuous I G.
proof: Proof. intros H H0. elim H; intros incF H'. elim H'; clear H H'; intros incG eqFG. elim H0; clear H0; intros incF' contF. split. auto. intros. apply Continuous_I_wd with F. FEQ. simpl in |- *; algebra. auto. Qed.
imports: CoRN.ftc.MoreIntervals