proposition: Lemma approximants_grow' : forall A X:Ensemble U, ~ Finite U A -> forall n:nat, cardinal U X n -> Approximant U A X -> exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
proof: Proof. intros A X H' n H'0 H'1; try assumption. elim H'1. intros H'2 H'3. cut (exists Y : _, cardinal U Y (S n) /\ Included U Y A). - intros [x H'4]; elim H'4; intros H'5 H'6; try exact H'5; clear H'4. exists x; auto with sets. split; [ auto with sets | idtac ]. apply Defn_of_Approximant; auto with sets. apply cardinal_finite with (n := S n); auto with sets. - apply approximants_grow with (X := X); auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image