proposition: Lemma subset_ordinal_cardinal_leq : forall u o, is_ordinal o -> sub u o -> ordinal_leq (cardinality u) o.
proof: Proof. ir. cp (wo_ordinal_obi_rw H). wr H1. ap ordinal_leq_subset_wo_ordinal. cp (ordinal_obi_next_compatible H). lu. rw obi_U. am. Qed.
imports: Arith ordinal