proposition: Lemma ordering_unbounded_unbounded : forall A B f, ordering_function f A B -> (Unbounded B <-> Unbounded A).
proof: Proof. Proof with auto with schutte. intros A B f H0;split. - intro; apply not_countable_unbounded. intro H2; assert (H3 : Countable B). { apply countable_bij_fun with Ord A f ... apply Ordering_bijection;auto. } case (countable_not_Unbounded H3);auto. - intro H1; apply not_countable_unbounded ... intro H2; assert (H3 : Countable A). { apply countable_bij_funR with Ord B f;auto. apply Ordering_bijection;auto. } case (countable_not_Unbounded (X:= A));auto. Qed.
imports: ZornsLemma(CountableTypes)