proposition: Lemma Included_imp_Diffble : forall J (pJ : proper J), included J I -> Diffble J pJ F.
proof: Proof. intros J pJ H. split. exact (included_trans _ _ _ _ H (Diffble_imp_inc _ diffF)). intros; apply included_imp_Diffble; Included. Qed.
imports: CoRN.ftc.MoreIntervals