proposition: Lemma closure_union: forall S T:Ensemble X, closure (Union S T) = Union (closure S) (closure T).
proof: Proof. intros. apply Extensionality_Ensembles; split. - apply closure_minimal. + apply closed_union2; apply closure_closed. + pose proof (closure_inflationary S). pose proof (closure_inflationary T). auto with sets. - assert (Included (closure S) (closure (Union S T))). { apply closure_increasing; auto with sets. } assert (Included (closure T) (closure (Union S T))). { apply closure_increasing; auto with sets. } auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)