proposition: Lemma closure_intersection: forall S T:Ensemble X, Included (closure (Intersection S T)) (Intersection (closure S) (closure T)).
proof: Proof. intros. assert (Included (closure (Intersection S T)) (closure S)). { apply closure_increasing; auto with sets. } assert (Included (closure (Intersection S T)) (closure T)). { apply closure_increasing; auto with sets. } auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)