proposition: Lemma make_new_approximant : forall A X:Ensemble U, ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
proof: Proof. intros A X H' H'0. elim H'0; intros H'1 H'2. apply Strict_super_set_contains_new_element; auto with sets. red; intro H'3; apply H'. rewrite <- H'3; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image