proposition: Theorem TH_13_6R (A B : Ensemble Ord) (f : Ord -> Ord) : ordering_function f A B -> Closed B -> Unbounded B -> normal f B.
proof: Proof. Proof with auto with schutte. intros H0 H1 H2; assert (A = ordinal). { apply segment_unbounded. - eapply SA1; apply H0. - destruct (ordering_unbounded_unbounded H0); auto. } subst A; split; [trivial | now apply Th_13_5_2]. Qed.
imports: ZornsLemma(CountableTypes)