proposition: Lemma Intersection_preserves_finite : forall A:Ensemble U, Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
proof: Proof. intros A H' X; apply Finite_downward_closed with A; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat