proposition: Lemma int_increasing: forall S1 S2:Ensemble X, Included S1 S2 -> Included (int S1) (int S2).
proof: Proof. intros. replace S1 with (Intersection S1 S2). - rewrite int_respects_intersection. auto with sets. - extensionality_ensembles; auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)