proposition: Theorem TH_13_6 (B : Ensemble Ord)(f : Ord -> Ord) : normal f B -> Closed B /\ Unbounded B.
proof: Proof. Proof with eauto with schutte. destruct 1. split. - eapply Th_13_5_1;eauto. - intros x; generalize (Ordering_bijection H). destruct 1 as [H3 H4 H5]. exists (f (succ x)); split. + apply H3 ... + apply le_lt_trans with (f x). * eapply ordering_le ... * eapply ordering_function_mono ... Qed.
imports: ZornsLemma(CountableTypes)